Metamath Proof Explorer

Theorem ifpbibib

Description: Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

Ref Expression
Assertion ifpbibib 
|- ( if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )

Proof

Step Hyp Ref Expression
1 dfifp2 
 |-  ( if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> ( ( ph -> ( ps <-> ch ) ) /\ ( -. ph -> ( th <-> ta ) ) ) )
2 dfbi2 
 |-  ( ( ps <-> ch ) <-> ( ( ps -> ch ) /\ ( ch -> ps ) ) )
3 2 imbi2i 
 |-  ( ( ph -> ( ps <-> ch ) ) <-> ( ph -> ( ( ps -> ch ) /\ ( ch -> ps ) ) ) )
4 jcab 
 |-  ( ( ph -> ( ( ps -> ch ) /\ ( ch -> ps ) ) ) <-> ( ( ph -> ( ps -> ch ) ) /\ ( ph -> ( ch -> ps ) ) ) )
5 3 4 bitri 
 |-  ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ( ps -> ch ) ) /\ ( ph -> ( ch -> ps ) ) ) )
6 dfbi2 
 |-  ( ( th <-> ta ) <-> ( ( th -> ta ) /\ ( ta -> th ) ) )
7 6 imbi2i 
 |-  ( ( -. ph -> ( th <-> ta ) ) <-> ( -. ph -> ( ( th -> ta ) /\ ( ta -> th ) ) ) )
8 jcab 
 |-  ( ( -. ph -> ( ( th -> ta ) /\ ( ta -> th ) ) ) <-> ( ( -. ph -> ( th -> ta ) ) /\ ( -. ph -> ( ta -> th ) ) ) )
9 7 8 bitri 
 |-  ( ( -. ph -> ( th <-> ta ) ) <-> ( ( -. ph -> ( th -> ta ) ) /\ ( -. ph -> ( ta -> th ) ) ) )
10 5 9 anbi12i 
 |-  ( ( ( ph -> ( ps <-> ch ) ) /\ ( -. ph -> ( th <-> ta ) ) ) <-> ( ( ( ph -> ( ps -> ch ) ) /\ ( ph -> ( ch -> ps ) ) ) /\ ( ( -. ph -> ( th -> ta ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) )
11 an4 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) /\ ( ph -> ( ch -> ps ) ) ) /\ ( ( -. ph -> ( th -> ta ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) <-> ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) /\ ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) )
12 10 11 bitri 
 |-  ( ( ( ph -> ( ps <-> ch ) ) /\ ( -. ph -> ( th <-> ta ) ) ) <-> ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) /\ ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) )
13 dfifp2 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) )
14 ifpimimb 
 |-  ( if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
15 13 14 bitr3i 
 |-  ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) <-> ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
16 dfifp2 
 |-  ( if- ( ph , ( ch -> ps ) , ( ta -> th ) ) <-> ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) )
17 ifpimimb 
 |-  ( if- ( ph , ( ch -> ps ) , ( ta -> th ) ) <-> ( if- ( ph , ch , ta ) -> if- ( ph , ps , th ) ) )
18 16 17 bitr3i 
 |-  ( ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) <-> ( if- ( ph , ch , ta ) -> if- ( ph , ps , th ) ) )
19 15 18 anbi12i 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) /\ ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) <-> ( ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) /\ ( if- ( ph , ch , ta ) -> if- ( ph , ps , th ) ) ) )
20 dfbi2 
 |-  ( ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) <-> ( ( if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) /\ ( if- ( ph , ch , ta ) -> if- ( ph , ps , th ) ) ) )
21 19 20 bitr4i 
 |-  ( ( ( ( ph -> ( ps -> ch ) ) /\ ( -. ph -> ( th -> ta ) ) ) /\ ( ( ph -> ( ch -> ps ) ) /\ ( -. ph -> ( ta -> th ) ) ) ) <-> ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
22 1 12 21 3bitri 
 |-  ( if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )