Metamath Proof Explorer

Theorem ifpim1

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

Ref Expression
Assertion ifpim1 
|- ( ( 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 imor 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
5 dfifp4 
 |-  ( if- ( -. ph , T. , ps ) <-> ( ( -. -. ph \/ T. ) /\ ( -. ph \/ ps ) ) )
6 3 4 5 3bitr4i 
 |-  ( ( ph -> ps ) <-> if- ( -. ph , T. , ps ) )