Metamath Proof Explorer

Theorem ifpim23g

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

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

Proof

Step Hyp Ref Expression
1 ifpidg 
 |-  ( ( ( ph -> ps ) <-> if- ( ch , ps , -. ph ) ) <-> ( ( ( ( ch /\ ps ) -> ( ph -> ps ) ) /\ ( ( ch /\ ( ph -> ps ) ) -> ps ) ) /\ ( ( -. ph -> ( ch \/ ( ph -> ps ) ) ) /\ ( ( ph -> ps ) -> ( ch \/ -. ph ) ) ) ) )
2 dfor2 
 |-  ( ( ph \/ ps ) <-> ( ( ph -> ps ) -> ps ) )
3 2 imbi2i 
 |-  ( ( ch -> ( ph \/ ps ) ) <-> ( ch -> ( ( ph -> ps ) -> ps ) ) )
4 impexp 
 |-  ( ( ( ch /\ ( ph -> ps ) ) -> ps ) <-> ( ch -> ( ( ph -> ps ) -> ps ) ) )
5 ax-1 
 |-  ( ps -> ( ph -> ps ) )
6 5 adantl 
 |-  ( ( ch /\ ps ) -> ( ph -> ps ) )
7 6 biantrur 
 |-  ( ( ( ch /\ ( ph -> ps ) ) -> ps ) <-> ( ( ( ch /\ ps ) -> ( ph -> ps ) ) /\ ( ( ch /\ ( ph -> ps ) ) -> ps ) ) )
8 3 4 7 3bitr2i 
 |-  ( ( ch -> ( ph \/ ps ) ) <-> ( ( ( ch /\ ps ) -> ( ph -> ps ) ) /\ ( ( ch /\ ( ph -> ps ) ) -> ps ) ) )
9 impexp 
 |-  ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )
10 imdi 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( ( ph -> ps ) -> ( ph -> ch ) ) )
11 imor 
 |-  ( ( ph -> ch ) <-> ( -. ph \/ ch ) )
12 orcom 
 |-  ( ( -. ph \/ ch ) <-> ( ch \/ -. ph ) )
13 11 12 bitri 
 |-  ( ( ph -> ch ) <-> ( ch \/ -. ph ) )
14 13 imbi2i 
 |-  ( ( ( ph -> ps ) -> ( ph -> ch ) ) <-> ( ( ph -> ps ) -> ( ch \/ -. ph ) ) )
15 10 14 bitri 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( ( ph -> ps ) -> ( ch \/ -. ph ) ) )
16 9 15 bitri 
 |-  ( ( ( ph /\ ps ) -> ch ) <-> ( ( ph -> ps ) -> ( ch \/ -. ph ) ) )
17 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
18 17 olcd 
 |-  ( -. ph -> ( ch \/ ( ph -> ps ) ) )
19 18 biantrur 
 |-  ( ( ( ph -> ps ) -> ( ch \/ -. ph ) ) <-> ( ( -. ph -> ( ch \/ ( ph -> ps ) ) ) /\ ( ( ph -> ps ) -> ( ch \/ -. ph ) ) ) )
20 16 19 bitri 
 |-  ( ( ( ph /\ ps ) -> ch ) <-> ( ( -. ph -> ( ch \/ ( ph -> ps ) ) ) /\ ( ( ph -> ps ) -> ( ch \/ -. ph ) ) ) )
21 8 20 anbi12i 
 |-  ( ( ( ch -> ( ph \/ ps ) ) /\ ( ( ph /\ ps ) -> ch ) ) <-> ( ( ( ( ch /\ ps ) -> ( ph -> ps ) ) /\ ( ( ch /\ ( ph -> ps ) ) -> ps ) ) /\ ( ( -. ph -> ( ch \/ ( ph -> ps ) ) ) /\ ( ( ph -> ps ) -> ( ch \/ -. ph ) ) ) ) )
22 ancom 
 |-  ( ( ( ch -> ( ph \/ ps ) ) /\ ( ( ph /\ ps ) -> ch ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ch -> ( ph \/ ps ) ) ) )
23 1 21 22 3bitr2i 
 |-  ( ( ( ph -> ps ) <-> if- ( ch , ps , -. ph ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ch -> ( ph \/ ps ) ) ) )