Metamath Proof Explorer

Theorem ifpid2

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpid2 
|- ( ph <-> if- ( ph , T. , F. ) )

Proof

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