Metamath Proof Explorer

Theorem ifpim123g

Description: Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020)

Ref Expression
Assertion ifpim123g ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfifp4 ⊢ ( if- ( 𝜑 , 𝜒 , 𝜏 ) ↔ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
2 dfifp4 ⊢ ( if- ( 𝜓 , 𝜃 , 𝜂 ) ↔ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) )
3 1 2 imbi12i ⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) → ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) )
4 imor ⊢ ( ( ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) → ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) ↔ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) )
5 ordi ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) ↔ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ¬ 𝜓 ∨ 𝜃 ) ) ∧ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( 𝜓 ∨ 𝜂 ) ) ) )
6 orass ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ¬ 𝜓 ) ∨ 𝜃 ) ↔ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ¬ 𝜓 ∨ 𝜃 ) ) )
7 ianor ⊢ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ↔ ( ¬ ( ¬ 𝜑 ∨ 𝜒 ) ∨ ¬ ( 𝜑 ∨ 𝜏 ) ) )
8 pm4.52 ⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) ↔ ¬ ( ¬ 𝜑 ∨ 𝜒 ) )
9 8 bicomi ⊢ ( ¬ ( ¬ 𝜑 ∨ 𝜒 ) ↔ ( 𝜑 ∧ ¬ 𝜒 ) )
10 ioran ⊢ ( ¬ ( 𝜑 ∨ 𝜏 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜏 ) )
11 9 10 orbi12i ⊢ ( ( ¬ ( ¬ 𝜑 ∨ 𝜒 ) ∨ ¬ ( 𝜑 ∨ 𝜏 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝜒 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜏 ) ) )
12 cases2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝜒 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜏 ) ) ↔ ( ( 𝜑 → ¬ 𝜒 ) ∧ ( ¬ 𝜑 → ¬ 𝜏 ) ) )
13 imor ⊢ ( ( 𝜑 → ¬ 𝜒 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜒 ) )
14 pm4.66 ⊢ ( ( ¬ 𝜑 → ¬ 𝜏 ) ↔ ( 𝜑 ∨ ¬ 𝜏 ) )
15 13 14 anbi12i ⊢ ( ( ( 𝜑 → ¬ 𝜒 ) ∧ ( ¬ 𝜑 → ¬ 𝜏 ) ) ↔ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) )
16 12 15 bitri ⊢ ( ( ( 𝜑 ∧ ¬ 𝜒 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜏 ) ) ↔ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) )
17 7 11 16 3bitri ⊢ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ↔ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) )
18 17 orbi1i ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ¬ 𝜓 ) ↔ ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ ¬ 𝜓 ) )
19 orcom ⊢ ( ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ ¬ 𝜓 ) ↔ ( ¬ 𝜓 ∨ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
20 ordi ⊢ ( ( ¬ 𝜓 ∨ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ) ↔ ( ( ¬ 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( ¬ 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
21 19 20 bitri ⊢ ( ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ ¬ 𝜓 ) ↔ ( ( ¬ 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( ¬ 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
22 orass ⊢ ( ( ( ¬ 𝜓 ∨ ¬ 𝜑 ) ∨ ¬ 𝜒 ) ↔ ( ¬ 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) )
23 orcom ⊢ ( ( ¬ 𝜓 ∨ ¬ 𝜑 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
24 imor ⊢ ( ( 𝜑 → ¬ 𝜓 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
25 23 24 bitr4i ⊢ ( ( ¬ 𝜓 ∨ ¬ 𝜑 ) ↔ ( 𝜑 → ¬ 𝜓 ) )
26 25 orbi1i ⊢ ( ( ( ¬ 𝜓 ∨ ¬ 𝜑 ) ∨ ¬ 𝜒 ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) )
27 22 26 bitr3i ⊢ ( ( ¬ 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) )
28 orass ⊢ ( ( ( ¬ 𝜓 ∨ 𝜑 ) ∨ ¬ 𝜏 ) ↔ ( ¬ 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) )
29 imor ⊢ ( ( 𝜓 → 𝜑 ) ↔ ( ¬ 𝜓 ∨ 𝜑 ) )
30 29 bicomi ⊢ ( ( ¬ 𝜓 ∨ 𝜑 ) ↔ ( 𝜓 → 𝜑 ) )
31 30 orbi1i ⊢ ( ( ( ¬ 𝜓 ∨ 𝜑 ) ∨ ¬ 𝜏 ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) )
32 28 31 bitr3i ⊢ ( ( ¬ 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) )
33 27 32 anbi12i ⊢ ( ( ( ¬ 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( ¬ 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) )
34 18 21 33 3bitri ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ¬ 𝜓 ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) )
35 34 orbi1i ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ¬ 𝜓 ) ∨ 𝜃 ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) ∨ 𝜃 ) )
36 ordir ⊢ ( ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) ∨ 𝜃 ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜃 ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜃 ) ) )
37 orass ⊢ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜃 ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 ∨ 𝜃 ) ) )
38 imor ⊢ ( ( 𝜒 → 𝜃 ) ↔ ( ¬ 𝜒 ∨ 𝜃 ) )
39 38 bicomi ⊢ ( ( ¬ 𝜒 ∨ 𝜃 ) ↔ ( 𝜒 → 𝜃 ) )
40 39 orbi2i ⊢ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 ∨ 𝜃 ) ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) )
41 37 40 bitri ⊢ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜃 ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) )
42 orass ⊢ ( ( ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜃 ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 ∨ 𝜃 ) ) )
43 imor ⊢ ( ( 𝜏 → 𝜃 ) ↔ ( ¬ 𝜏 ∨ 𝜃 ) )
44 43 bicomi ⊢ ( ( ¬ 𝜏 ∨ 𝜃 ) ↔ ( 𝜏 → 𝜃 ) )
45 44 orbi2i ⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 ∨ 𝜃 ) ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) )
46 42 45 bitri ⊢ ( ( ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜃 ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) )
47 41 46 anbi12i ⊢ ( ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜃 ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜃 ) ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) )
48 35 36 47 3bitri ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ¬ 𝜓 ) ∨ 𝜃 ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) )
49 6 48 bitr3i ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ¬ 𝜓 ∨ 𝜃 ) ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) )
50 orass ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ 𝜓 ) ∨ 𝜂 ) ↔ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( 𝜓 ∨ 𝜂 ) ) )
51 17 orbi1i ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ 𝜓 ) ↔ ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ 𝜓 ) )
52 orcom ⊢ ( ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ 𝜓 ) ↔ ( 𝜓 ∨ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
53 ordi ⊢ ( ( 𝜓 ∨ ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ) ↔ ( ( 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
54 52 53 bitri ⊢ ( ( ( ( ¬ 𝜑 ∨ ¬ 𝜒 ) ∧ ( 𝜑 ∨ ¬ 𝜏 ) ) ∨ 𝜓 ) ↔ ( ( 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) )
55 orass ⊢ ( ( ( 𝜓 ∨ ¬ 𝜑 ) ∨ ¬ 𝜒 ) ↔ ( 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) )
56 orcom ⊢ ( ( 𝜓 ∨ ¬ 𝜑 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) )
57 imor ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) )
58 56 57 bitr4i ⊢ ( ( 𝜓 ∨ ¬ 𝜑 ) ↔ ( 𝜑 → 𝜓 ) )
59 58 orbi1i ⊢ ( ( ( 𝜓 ∨ ¬ 𝜑 ) ∨ ¬ 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) )
60 55 59 bitr3i ⊢ ( ( 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) )
61 orass ⊢ ( ( ( 𝜓 ∨ 𝜑 ) ∨ ¬ 𝜏 ) ↔ ( 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) )
62 df-or ⊢ ( ( 𝜓 ∨ 𝜑 ) ↔ ( ¬ 𝜓 → 𝜑 ) )
63 62 orbi1i ⊢ ( ( ( 𝜓 ∨ 𝜑 ) ∨ ¬ 𝜏 ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) )
64 61 63 bitr3i ⊢ ( ( 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) )
65 60 64 anbi12i ⊢ ( ( ( 𝜓 ∨ ( ¬ 𝜑 ∨ ¬ 𝜒 ) ) ∧ ( 𝜓 ∨ ( 𝜑 ∨ ¬ 𝜏 ) ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) )
66 51 54 65 3bitri ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ 𝜓 ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) )
67 66 orbi1i ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ 𝜓 ) ∨ 𝜂 ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) ∨ 𝜂 ) )
68 ordir ⊢ ( ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ) ∨ 𝜂 ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜂 ) ∧ ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜂 ) ) )
69 orass ⊢ ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜂 ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 ∨ 𝜂 ) ) )
70 imor ⊢ ( ( 𝜒 → 𝜂 ) ↔ ( ¬ 𝜒 ∨ 𝜂 ) )
71 70 bicomi ⊢ ( ( ¬ 𝜒 ∨ 𝜂 ) ↔ ( 𝜒 → 𝜂 ) )
72 71 orbi2i ⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 ∨ 𝜂 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) )
73 69 72 bitri ⊢ ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜂 ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) )
74 orass ⊢ ( ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜂 ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 ∨ 𝜂 ) ) )
75 imor ⊢ ( ( 𝜏 → 𝜂 ) ↔ ( ¬ 𝜏 ∨ 𝜂 ) )
76 75 bicomi ⊢ ( ( ¬ 𝜏 ∨ 𝜂 ) ↔ ( 𝜏 → 𝜂 ) )
77 76 orbi2i ⊢ ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 ∨ 𝜂 ) ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) )
78 74 77 bitri ⊢ ( ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜂 ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) )
79 73 78 anbi12i ⊢ ( ( ( ( ( 𝜑 → 𝜓 ) ∨ ¬ 𝜒 ) ∨ 𝜂 ) ∧ ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ¬ 𝜏 ) ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) )
80 67 68 79 3bitri ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ 𝜓 ) ∨ 𝜂 ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) )
81 50 80 bitr3i ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( 𝜓 ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) )
82 49 81 anbi12i ⊢ ( ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ¬ 𝜓 ∨ 𝜃 ) ) ∧ ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( 𝜓 ∨ 𝜂 ) ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) ) )
83 5 82 bitri ⊢ ( ( ¬ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∨ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) ) )
84 3 4 83 3bitri ⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 → 𝜂 ) ) ) ) )