Metamath Proof Explorer

Theorem ifpidg

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

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

Proof

Step Hyp Ref Expression
1 dfifp4 
 |-  ( if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) )
2 1 bibi2i 
 |-  ( ( th <-> if- ( ph , ps , ch ) ) <-> ( th <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) )
3 dfbi2 
 |-  ( ( th <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) <-> ( ( th -> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) /\ ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) -> th ) ) )
4 imor 
 |-  ( ( th -> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) <-> ( -. th \/ ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) )
5 ordi 
 |-  ( ( -. th \/ ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) <-> ( ( -. th \/ ( -. ph \/ ps ) ) /\ ( -. th \/ ( ph \/ ch ) ) ) )
6 ancomst 
 |-  ( ( ( ph /\ th ) -> ps ) <-> ( ( th /\ ph ) -> ps ) )
7 impexp 
 |-  ( ( ( th /\ ph ) -> ps ) <-> ( th -> ( ph -> ps ) ) )
8 imor 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
9 8 imbi2i 
 |-  ( ( th -> ( ph -> ps ) ) <-> ( th -> ( -. ph \/ ps ) ) )
10 imor 
 |-  ( ( th -> ( -. ph \/ ps ) ) <-> ( -. th \/ ( -. ph \/ ps ) ) )
11 9 10 bitri 
 |-  ( ( th -> ( ph -> ps ) ) <-> ( -. th \/ ( -. ph \/ ps ) ) )
12 6 7 11 3bitrri 
 |-  ( ( -. th \/ ( -. ph \/ ps ) ) <-> ( ( ph /\ th ) -> ps ) )
13 imor 
 |-  ( ( th -> ( ph \/ ch ) ) <-> ( -. th \/ ( ph \/ ch ) ) )
14 13 bicomi 
 |-  ( ( -. th \/ ( ph \/ ch ) ) <-> ( th -> ( ph \/ ch ) ) )
15 12 14 anbi12i 
 |-  ( ( ( -. th \/ ( -. ph \/ ps ) ) /\ ( -. th \/ ( ph \/ ch ) ) ) <-> ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) )
16 4 5 15 3bitri 
 |-  ( ( th -> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) <-> ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) )
17 8 bicomi 
 |-  ( ( -. ph \/ ps ) <-> ( ph -> ps ) )
18 df-or 
 |-  ( ( ph \/ ch ) <-> ( -. ph -> ch ) )
19 17 18 anbi12i 
 |-  ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
20 cases2 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
21 20 bicomi 
 |-  ( ( ( ph -> ps ) /\ ( -. ph -> ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
22 19 21 bitri 
 |-  ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
23 22 imbi1i 
 |-  ( ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) -> th ) <-> ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> th ) )
24 jaob 
 |-  ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> th ) <-> ( ( ( ph /\ ps ) -> th ) /\ ( ( -. ph /\ ch ) -> th ) ) )
25 ancomst 
 |-  ( ( ( -. ph /\ ch ) -> th ) <-> ( ( ch /\ -. ph ) -> th ) )
26 pm5.6 
 |-  ( ( ( ch /\ -. ph ) -> th ) <-> ( ch -> ( ph \/ th ) ) )
27 25 26 bitri 
 |-  ( ( ( -. ph /\ ch ) -> th ) <-> ( ch -> ( ph \/ th ) ) )
28 27 anbi2i 
 |-  ( ( ( ( ph /\ ps ) -> th ) /\ ( ( -. ph /\ ch ) -> th ) ) <-> ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) )
29 23 24 28 3bitri 
 |-  ( ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) -> th ) <-> ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) )
30 16 29 anbi12i 
 |-  ( ( ( th -> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) /\ ( ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) -> th ) ) <-> ( ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) ) )
31 3 30 bitri 
 |-  ( ( th <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) <-> ( ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) ) )
32 ancom 
 |-  ( ( ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) /\ ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) ) )
33 an4 
 |-  ( ( ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) /\ ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ( ph /\ th ) -> ps ) ) /\ ( ( ch -> ( ph \/ th ) ) /\ ( th -> ( ph \/ ch ) ) ) ) )
34 32 33 bitri 
 |-  ( ( ( ( ( ph /\ th ) -> ps ) /\ ( th -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> th ) /\ ( ch -> ( ph \/ th ) ) ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ( ph /\ th ) -> ps ) ) /\ ( ( ch -> ( ph \/ th ) ) /\ ( th -> ( ph \/ ch ) ) ) ) )
35 2 31 34 3bitri 
 |-  ( ( th <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ( ph /\ th ) -> ps ) ) /\ ( ( ch -> ( ph \/ th ) ) /\ ( th -> ( ph \/ ch ) ) ) ) )