Metamath Proof Explorer

Theorem biort

Description: A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999)

Ref Expression
Assertion biort 
|- ( ph -> ( ph <-> ( ph \/ ps ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ph -> ph )
2 orc 
 |-  ( ph -> ( ph \/ ps ) )
3 1 2 2thd 
 |-  ( ph -> ( ph <-> ( ph \/ ps ) ) )