Theorem orfa 33881

Description: The falsum F. can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)

Assertion

Ref	Expression
orfa	|- ( ( ph \/ F. ) <-> ph )

Proof of Theorem orfa

Step	Hyp	Ref	Expression
1		orcom 402	. . . 4 |- ( ( ph \/ F. ) <-> ( F. \/ ph ) )
2		df-or 385	. . . 4 |- ( ( F. \/ ph ) <-> ( -. F. -> ph ) )
3	1, 2	bitri 264	. . 3 |- ( ( ph \/ F. ) <-> ( -. F. -> ph ) )
4		fal 1490	. . . 4 |- -. F.
5		pm2.27 42	. . . 4 |- ( -. F. -> ( ( -. F. -> ph ) -> ph ) )
6	4, 5	ax-mp 5	. . 3 |- ( ( -. F. -> ph ) -> ph )
7	3, 6	sylbi 207	. 2 |- ( ( ph \/ F. ) -> ph )
8		orc 400	. 2 |- ( ph -> ( ph \/ F. ) )
9	7, 8	impbii 199	1 |- ( ( ph \/ F. ) <-> ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   F. wfal 1488

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-tru 1486  df-fal 1489

This theorem is referenced by: (None)