Theorem biorf 807

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 803	. 2 |- (-. ph -> (ps <-> (-. ph -> ps)))
2		df-or 241	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	syl6bbr 597	1 |- (-. ph -> (ps <-> (ph \/ ps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239

This theorem is referenced by:  biorfi 808  19.33b 1444  19.33bOLD 1445  euor 1793  unineq 2844  disjssunOLD 2933  difprsn 3127  iununi 3331  iununiOLD 3332  opthwiener 3554  opthprc 4046  ltxrlt 6669  ne0gt0 6801  xrsupss 7287  xrinfmss 7288  nmlnogt0 9797  pilem1 10020  hvmulcan 10571  hvmulcanOLD 10572  hvmulcan2 10573  coprm 13782  elpadd0 17270

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 164  df-or 241  df-an 242

Copyright terms: Public domain