Metamath Proof Explorer

Theorem ifpnot

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

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

Proof

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