Theorem biorf 733

Description: A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121.

Assertion

Ref	Expression
biorf	|- (-. ph -> (ps <-> (ph \/ ps)))

Proof of Theorem biorf

Step	Hyp	Ref	Expression
1		biimt 729	. 2 |- (-. ph -> (ps <-> (-. ph -> ps)))
2		df-or 224	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	syl6bbr 536	1 |- (-. ph -> (ps <-> (ph \/ ps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222

This theorem is referenced by:  biorfi 734  19.33b 1088  euor 1391  unineq 2245  disjssun 2316  iununi 2606  opthwiener 2796  opthprc 3211  ltxrltt 5472  ne0gt0t 5593  xrsupss 6025  xrinfmss 6026  nmlnogt0 8389  pilem1 8590  hvmulcant 8860  hvmulcan2t 8861

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain