Metamath Proof Explorer

Theorem ifpdfor

Description: Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpdfor 
|- ( ( ph \/ ps ) <-> if- ( ph , T. , ps ) )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 1 olci 
 |-  ( -. ph \/ T. )
3 2 biantrur 
 |-  ( ( ph \/ ps ) <-> ( ( -. ph \/ T. ) /\ ( ph \/ ps ) ) )
4 dfifp4 
 |-  ( if- ( ph , T. , ps ) <-> ( ( -. ph \/ T. ) /\ ( ph \/ ps ) ) )
5 3 4 bitr4i 
 |-  ( ( ph \/ ps ) <-> if- ( ph , T. , ps ) )