Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpim123g Structured version   Visualization version   GIF version

Theorem ifpim123g 38521
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.)
Assertion
Ref Expression
ifpim123g ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))

Proof of Theorem ifpim123g
StepHypRef Expression
1 dfifp4 1089 . . 3 (if-(𝜑, 𝜒, 𝜏) ↔ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)))
2 dfifp4 1089 . . 3 (if-(𝜓, 𝜃, 𝜂) ↔ ((¬ 𝜓𝜃) ∧ (𝜓𝜂)))
31, 2imbi12i 341 . 2 ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑𝜒) ∧ (𝜑𝜏)) → ((¬ 𝜓𝜃) ∧ (𝜓𝜂))))
4 imor 879 . 2 ((((¬ 𝜑𝜒) ∧ (𝜑𝜏)) → ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))))
5 ordi 1028 . . 3 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ∧ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂))))
6 orass 945 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)))
7 ianor 1004 . . . . . . . . . 10 (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ↔ (¬ (¬ 𝜑𝜒) ∨ ¬ (𝜑𝜏)))
8 pm4.52 1007 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝜒) ↔ ¬ (¬ 𝜑𝜒))
98bicomi 215 . . . . . . . . . . 11 (¬ (¬ 𝜑𝜒) ↔ (𝜑 ∧ ¬ 𝜒))
10 ioran 1006 . . . . . . . . . . 11 (¬ (𝜑𝜏) ↔ (¬ 𝜑 ∧ ¬ 𝜏))
119, 10orbi12i 938 . . . . . . . . . 10 ((¬ (¬ 𝜑𝜒) ∨ ¬ (𝜑𝜏)) ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)))
12 cases2 1070 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)))
13 imor 879 . . . . . . . . . . . 12 ((𝜑 → ¬ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜒))
14 pm4.66 876 . . . . . . . . . . . 12 ((¬ 𝜑 → ¬ 𝜏) ↔ (𝜑 ∨ ¬ 𝜏))
1513, 14anbi12i 620 . . . . . . . . . . 11 (((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
1612, 15bitri 266 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
177, 11, 163bitri 288 . . . . . . . . 9 (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
1817orbi1i 937 . . . . . . . 8 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓))
19 orcom 896 . . . . . . . . 9 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ (¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
20 ordi 1028 . . . . . . . . 9 ((¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
2119, 20bitri 266 . . . . . . . 8 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
22 orass 945 . . . . . . . . . 10 (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
23 orcom 896 . . . . . . . . . . . 12 ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
24 imor 879 . . . . . . . . . . . 12 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
2523, 24bitr4i 269 . . . . . . . . . . 11 ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → ¬ 𝜓))
2625orbi1i 937 . . . . . . . . . 10 (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
2722, 26bitr3i 268 . . . . . . . . 9 ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
28 orass 945 . . . . . . . . . 10 (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ↔ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
29 imor 879 . . . . . . . . . . . 12 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
3029bicomi 215 . . . . . . . . . . 11 ((¬ 𝜓𝜑) ↔ (𝜓𝜑))
3130orbi1i 937 . . . . . . . . . 10 (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ↔ ((𝜓𝜑) ∨ ¬ 𝜏))
3228, 31bitr3i 268 . . . . . . . . 9 ((¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((𝜓𝜑) ∨ ¬ 𝜏))
3327, 32anbi12i 620 . . . . . . . 8 (((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)))
3418, 21, 333bitri 288 . . . . . . 7 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)))
3534orbi1i 937 . . . . . 6 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜃))
36 ordir 1029 . . . . . 6 (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃)))
37 orass 945 . . . . . . . 8 ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒𝜃)))
38 imor 879 . . . . . . . . . 10 ((𝜒𝜃) ↔ (¬ 𝜒𝜃))
3938bicomi 215 . . . . . . . . 9 ((¬ 𝜒𝜃) ↔ (𝜒𝜃))
4039orbi2i 936 . . . . . . . 8 (((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒𝜃)) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)))
4137, 40bitri 266 . . . . . . 7 ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)))
42 orass 945 . . . . . . . 8 ((((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓𝜑) ∨ (¬ 𝜏𝜃)))
43 imor 879 . . . . . . . . . 10 ((𝜏𝜃) ↔ (¬ 𝜏𝜃))
4443bicomi 215 . . . . . . . . 9 ((¬ 𝜏𝜃) ↔ (𝜏𝜃))
4544orbi2i 936 . . . . . . . 8 (((𝜓𝜑) ∨ (¬ 𝜏𝜃)) ↔ ((𝜓𝜑) ∨ (𝜏𝜃)))
4642, 45bitri 266 . . . . . . 7 ((((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓𝜑) ∨ (𝜏𝜃)))
4741, 46anbi12i 620 . . . . . 6 (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
4835, 36, 473bitri 288 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
496, 48bitr3i 268 . . . 4 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
50 orass 945 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂)))
5117orbi1i 937 . . . . . . . 8 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓))
52 orcom 896 . . . . . . . . 9 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ (𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
53 ordi 1028 . . . . . . . . 9 ((𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
5452, 53bitri 266 . . . . . . . 8 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
55 orass 945 . . . . . . . . . 10 (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
56 orcom 896 . . . . . . . . . . . 12 ((𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑𝜓))
57 imor 879 . . . . . . . . . . . 12 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
5856, 57bitr4i 269 . . . . . . . . . . 11 ((𝜓 ∨ ¬ 𝜑) ↔ (𝜑𝜓))
5958orbi1i 937 . . . . . . . . . 10 (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑𝜓) ∨ ¬ 𝜒))
6055, 59bitr3i 268 . . . . . . . . 9 ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑𝜓) ∨ ¬ 𝜒))
61 orass 945 . . . . . . . . . 10 (((𝜓𝜑) ∨ ¬ 𝜏) ↔ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
62 df-or 874 . . . . . . . . . . 11 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
6362orbi1i 937 . . . . . . . . . 10 (((𝜓𝜑) ∨ ¬ 𝜏) ↔ ((¬ 𝜓𝜑) ∨ ¬ 𝜏))
6461, 63bitr3i 268 . . . . . . . . 9 ((𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((¬ 𝜓𝜑) ∨ ¬ 𝜏))
6560, 64anbi12i 620 . . . . . . . 8 (((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)))
6651, 54, 653bitri 288 . . . . . . 7 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ↔ (((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)))
6766orbi1i 937 . . . . . 6 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ ((((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜂))
68 ordir 1029 . . . . . 6 (((((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜂) ↔ ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂)))
69 orass 945 . . . . . . . 8 ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑𝜓) ∨ (¬ 𝜒𝜂)))
70 imor 879 . . . . . . . . . 10 ((𝜒𝜂) ↔ (¬ 𝜒𝜂))
7170bicomi 215 . . . . . . . . 9 ((¬ 𝜒𝜂) ↔ (𝜒𝜂))
7271orbi2i 936 . . . . . . . 8 (((𝜑𝜓) ∨ (¬ 𝜒𝜂)) ↔ ((𝜑𝜓) ∨ (𝜒𝜂)))
7369, 72bitri 266 . . . . . . 7 ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑𝜓) ∨ (𝜒𝜂)))
74 orass 945 . . . . . . . 8 ((((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓𝜑) ∨ (¬ 𝜏𝜂)))
75 imor 879 . . . . . . . . . 10 ((𝜏𝜂) ↔ (¬ 𝜏𝜂))
7675bicomi 215 . . . . . . . . 9 ((¬ 𝜏𝜂) ↔ (𝜏𝜂))
7776orbi2i 936 . . . . . . . 8 (((¬ 𝜓𝜑) ∨ (¬ 𝜏𝜂)) ↔ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))
7874, 77bitri 266 . . . . . . 7 ((((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))
7973, 78anbi12i 620 . . . . . 6 (((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂)) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8067, 68, 793bitri 288 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8150, 80bitr3i 268 . . . 4 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂)) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8249, 81anbi12i 620 . . 3 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ∧ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
835, 82bitri 266 . 2 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
843, 4, 833bitri 288 1 ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  if-wif 1085
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ifp 1086
This theorem is referenced by:  ifpim1g  38522  ifpbi1b  38524  ifpimimb  38525  ifpor123g  38529  ifpimim  38530
  Copyright terms: Public domain W3C validator