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-ψθη↔φ→¬ψ∨χ→θ∧ψ→φ∨τ→θ∧φ→ψ∨χ→η∧¬ψ→φ∨τ→η