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