Metamath Proof Explorer

Theorem ifpdfor2

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

Ref Expression
Assertion ifpdfor2 
|- ( ( ph \/ ps ) <-> if- ( ph , ph , ps ) )

Proof

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