Theorem biorf 734

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 730	. 2 |- (-. ph -> (ps <-> (-. ph -> ps)))
2		df-or 224	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	syl6bbr 537	1 |- (-. ph -> (ps <-> (ph \/ ps)))

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

This theorem is referenced by:  biorfi 735  19.33b 1090  euor 1396  unineq 2251  disjssun 2322  iununi 2611  opthwiener 2802  opthprc 3216  ltxrltt 5480  ne0gt0t 5601  xrsupss 6033  xrinfmss 6034  nmlnogt0 8402  pilem1 8609  hvmulcant 8878  hvmulcan2t 8879

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