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- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 dfifp2 ⊢ ( if- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ↔ 𝜏 ) ) ) )
2 dfbi2 ⊢ ( ( 𝜓 ↔ 𝜒 ) ↔ ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
3 2 imbi2i ⊢ ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ↔ ( 𝜑 → ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) ) )
4 jcab ⊢ ( ( 𝜑 → ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) ) ↔ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( 𝜑 → ( 𝜒 → 𝜓 ) ) ) )
5 3 4 bitri ⊢ ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ↔ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( 𝜑 → ( 𝜒 → 𝜓 ) ) ) )
6 dfbi2 ⊢ ( ( 𝜃 ↔ 𝜏 ) ↔ ( ( 𝜃 → 𝜏 ) ∧ ( 𝜏 → 𝜃 ) ) )
7 6 imbi2i ⊢ ( ( ¬ 𝜑 → ( 𝜃 ↔ 𝜏 ) ) ↔ ( ¬ 𝜑 → ( ( 𝜃 → 𝜏 ) ∧ ( 𝜏 → 𝜃 ) ) ) )
8 jcab ⊢ ( ( ¬ 𝜑 → ( ( 𝜃 → 𝜏 ) ∧ ( 𝜏 → 𝜃 ) ) ) ↔ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) )
9 7 8 bitri ⊢ ( ( ¬ 𝜑 → ( 𝜃 ↔ 𝜏 ) ) ↔ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) )
10 5 9 anbi12i ⊢ ( ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ↔ 𝜏 ) ) ) ↔ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( 𝜑 → ( 𝜒 → 𝜓 ) ) ) ∧ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) )
11 an4 ⊢ ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( 𝜑 → ( 𝜒 → 𝜓 ) ) ) ∧ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) ↔ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ∧ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) )
12 10 11 bitri ⊢ ( ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ↔ 𝜏 ) ) ) ↔ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ∧ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) )
13 dfifp2 ⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) )
14 ifpimimb ⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
15 13 14 bitr3i ⊢ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
16 dfifp2 ⊢ ( if- ( 𝜑 , ( 𝜒 → 𝜓 ) , ( 𝜏 → 𝜃 ) ) ↔ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) )
17 ifpimimb ⊢ ( if- ( 𝜑 , ( 𝜒 → 𝜓 ) , ( 𝜏 → 𝜃 ) ) ↔ ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜑 , 𝜓 , 𝜃 ) ) )
18 16 17 bitr3i ⊢ ( ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ↔ ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜑 , 𝜓 , 𝜃 ) ) )
19 15 18 anbi12i ⊢ ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ∧ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) ↔ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ∧ ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜑 , 𝜓 , 𝜃 ) ) ) )
20 dfbi2 ⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ∧ ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜑 , 𝜓 , 𝜃 ) ) ) )
21 19 20 bitr4i ⊢ ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ∧ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) ∧ ( ¬ 𝜑 → ( 𝜏 → 𝜃 ) ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
22 1 12 21 3bitri ⊢ ( if- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )