Metamath Proof Explorer

Theorem orfa

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

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

Proof

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