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 37326
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 1015 . . 3 (if-(𝜑, 𝜒, 𝜏) ↔ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)))
2 dfifp4 1015 . . 3 (if-(𝜓, 𝜃, 𝜂) ↔ ((¬ 𝜓𝜃) ∧ (𝜓𝜂)))
31, 2imbi12i 340 . 2 ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑𝜒) ∧ (𝜑𝜏)) → ((¬ 𝜓𝜃) ∧ (𝜓𝜂))))
4 imor 428 . 2 ((((¬ 𝜑𝜒) ∧ (𝜑𝜏)) → ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))))
5 ordi 907 . . 3 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ∧ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂))))
6 orass 546 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)))
7 ianor 509 . . . . . . . . . 10 (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ↔ (¬ (¬ 𝜑𝜒) ∨ ¬ (𝜑𝜏)))
8 pm4.52 512 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝜒) ↔ ¬ (¬ 𝜑𝜒))
98bicomi 214 . . . . . . . . . . 11 (¬ (¬ 𝜑𝜒) ↔ (𝜑 ∧ ¬ 𝜒))
10 ioran 511 . . . . . . . . . . 11 (¬ (𝜑𝜏) ↔ (¬ 𝜑 ∧ ¬ 𝜏))
119, 10orbi12i 543 . . . . . . . . . 10 ((¬ (¬ 𝜑𝜒) ∨ ¬ (𝜑𝜏)) ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)))
12 cases2 992 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)))
13 imor 428 . . . . . . . . . . . 12 ((𝜑 → ¬ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜒))
14 pm4.66 436 . . . . . . . . . . . 12 ((¬ 𝜑 → ¬ 𝜏) ↔ (𝜑 ∨ ¬ 𝜏))
1513, 14anbi12i 732 . . . . . . . . . . 11 (((𝜑 → ¬ 𝜒) ∧ (¬ 𝜑 → ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
1612, 15bitri 264 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝜒) ∨ (¬ 𝜑 ∧ ¬ 𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
177, 11, 163bitri 286 . . . . . . . . 9 (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ↔ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)))
1817orbi1i 542 . . . . . . . 8 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓))
19 orcom 402 . . . . . . . . 9 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ (¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
20 ordi 907 . . . . . . . . 9 ((¬ 𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
2119, 20bitri 264 . . . . . . . 8 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ ¬ 𝜓) ↔ ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
22 orass 546 . . . . . . . . . 10 (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
23 orcom 402 . . . . . . . . . . . 12 ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
24 imor 428 . . . . . . . . . . . 12 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
2523, 24bitr4i 267 . . . . . . . . . . 11 ((¬ 𝜓 ∨ ¬ 𝜑) ↔ (𝜑 → ¬ 𝜓))
2625orbi1i 542 . . . . . . . . . 10 (((¬ 𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
2722, 26bitr3i 266 . . . . . . . . 9 ((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒))
28 orass 546 . . . . . . . . . 10 (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ↔ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
29 imor 428 . . . . . . . . . . . 12 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
3029bicomi 214 . . . . . . . . . . 11 ((¬ 𝜓𝜑) ↔ (𝜓𝜑))
3130orbi1i 542 . . . . . . . . . 10 (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ↔ ((𝜓𝜑) ∨ ¬ 𝜏))
3228, 31bitr3i 266 . . . . . . . . 9 ((¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((𝜓𝜑) ∨ ¬ 𝜏))
3327, 32anbi12i 732 . . . . . . . 8 (((¬ 𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (¬ 𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)))
3418, 21, 333bitri 286 . . . . . . 7 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ↔ (((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)))
3534orbi1i 542 . . . . . 6 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜃))
36 ordir 908 . . . . . 6 (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∧ ((𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜃) ↔ ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃)))
37 orass 546 . . . . . . . 8 ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒𝜃)))
38 imor 428 . . . . . . . . . 10 ((𝜒𝜃) ↔ (¬ 𝜒𝜃))
3938bicomi 214 . . . . . . . . 9 ((¬ 𝜒𝜃) ↔ (𝜒𝜃))
4039orbi2i 541 . . . . . . . 8 (((𝜑 → ¬ 𝜓) ∨ (¬ 𝜒𝜃)) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)))
4137, 40bitri 264 . . . . . . 7 ((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ↔ ((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)))
42 orass 546 . . . . . . . 8 ((((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓𝜑) ∨ (¬ 𝜏𝜃)))
43 imor 428 . . . . . . . . . 10 ((𝜏𝜃) ↔ (¬ 𝜏𝜃))
4443bicomi 214 . . . . . . . . 9 ((¬ 𝜏𝜃) ↔ (𝜏𝜃))
4544orbi2i 541 . . . . . . . 8 (((𝜓𝜑) ∨ (¬ 𝜏𝜃)) ↔ ((𝜓𝜑) ∨ (𝜏𝜃)))
4642, 45bitri 264 . . . . . . 7 ((((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃) ↔ ((𝜓𝜑) ∨ (𝜏𝜃)))
4741, 46anbi12i 732 . . . . . 6 (((((𝜑 → ¬ 𝜓) ∨ ¬ 𝜒) ∨ 𝜃) ∧ (((𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
4835, 36, 473bitri 286 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ¬ 𝜓) ∨ 𝜃) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
496, 48bitr3i 266 . . . 4 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ↔ (((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))))
50 orass 546 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂)))
5117orbi1i 542 . . . . . . . 8 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ↔ (((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓))
52 orcom 402 . . . . . . . . 9 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ (𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))))
53 ordi 907 . . . . . . . . 9 ((𝜓 ∨ ((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏))) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
5452, 53bitri 264 . . . . . . . 8 ((((¬ 𝜑 ∨ ¬ 𝜒) ∧ (𝜑 ∨ ¬ 𝜏)) ∨ 𝜓) ↔ ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))))
55 orass 546 . . . . . . . . . 10 (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ (𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)))
56 orcom 402 . . . . . . . . . . . 12 ((𝜓 ∨ ¬ 𝜑) ↔ (¬ 𝜑𝜓))
57 imor 428 . . . . . . . . . . . 12 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
5856, 57bitr4i 267 . . . . . . . . . . 11 ((𝜓 ∨ ¬ 𝜑) ↔ (𝜑𝜓))
5958orbi1i 542 . . . . . . . . . 10 (((𝜓 ∨ ¬ 𝜑) ∨ ¬ 𝜒) ↔ ((𝜑𝜓) ∨ ¬ 𝜒))
6055, 59bitr3i 266 . . . . . . . . 9 ((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ↔ ((𝜑𝜓) ∨ ¬ 𝜒))
61 orass 546 . . . . . . . . . 10 (((𝜓𝜑) ∨ ¬ 𝜏) ↔ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏)))
62 df-or 385 . . . . . . . . . . 11 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
6362orbi1i 542 . . . . . . . . . 10 (((𝜓𝜑) ∨ ¬ 𝜏) ↔ ((¬ 𝜓𝜑) ∨ ¬ 𝜏))
6461, 63bitr3i 266 . . . . . . . . 9 ((𝜓 ∨ (𝜑 ∨ ¬ 𝜏)) ↔ ((¬ 𝜓𝜑) ∨ ¬ 𝜏))
6560, 64anbi12i 732 . . . . . . . 8 (((𝜓 ∨ (¬ 𝜑 ∨ ¬ 𝜒)) ∧ (𝜓 ∨ (𝜑 ∨ ¬ 𝜏))) ↔ (((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)))
6651, 54, 653bitri 286 . . . . . . 7 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ↔ (((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)))
6766orbi1i 542 . . . . . 6 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ ((((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜂))
68 ordir 908 . . . . . 6 (((((𝜑𝜓) ∨ ¬ 𝜒) ∧ ((¬ 𝜓𝜑) ∨ ¬ 𝜏)) ∨ 𝜂) ↔ ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂)))
69 orass 546 . . . . . . . 8 ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑𝜓) ∨ (¬ 𝜒𝜂)))
70 imor 428 . . . . . . . . . 10 ((𝜒𝜂) ↔ (¬ 𝜒𝜂))
7170bicomi 214 . . . . . . . . 9 ((¬ 𝜒𝜂) ↔ (𝜒𝜂))
7271orbi2i 541 . . . . . . . 8 (((𝜑𝜓) ∨ (¬ 𝜒𝜂)) ↔ ((𝜑𝜓) ∨ (𝜒𝜂)))
7369, 72bitri 264 . . . . . . 7 ((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ↔ ((𝜑𝜓) ∨ (𝜒𝜂)))
74 orass 546 . . . . . . . 8 ((((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓𝜑) ∨ (¬ 𝜏𝜂)))
75 imor 428 . . . . . . . . . 10 ((𝜏𝜂) ↔ (¬ 𝜏𝜂))
7675bicomi 214 . . . . . . . . 9 ((¬ 𝜏𝜂) ↔ (𝜏𝜂))
7776orbi2i 541 . . . . . . . 8 (((¬ 𝜓𝜑) ∨ (¬ 𝜏𝜂)) ↔ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))
7874, 77bitri 264 . . . . . . 7 ((((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂) ↔ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))
7973, 78anbi12i 732 . . . . . 6 (((((𝜑𝜓) ∨ ¬ 𝜒) ∨ 𝜂) ∧ (((¬ 𝜓𝜑) ∨ ¬ 𝜏) ∨ 𝜂)) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8067, 68, 793bitri 286 . . . . 5 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ 𝜓) ∨ 𝜂) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8150, 80bitr3i 266 . . . 4 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂)) ↔ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂))))
8249, 81anbi12i 732 . . 3 (((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (¬ 𝜓𝜃)) ∧ (¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ (𝜓𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
835, 82bitri 264 . 2 ((¬ ((¬ 𝜑𝜒) ∧ (𝜑𝜏)) ∨ ((¬ 𝜓𝜃) ∧ (𝜓𝜂))) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
843, 4, 833bitri 286 1 ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒𝜃)) ∧ ((𝜓𝜑) ∨ (𝜏𝜃))) ∧ (((𝜑𝜓) ∨ (𝜒𝜂)) ∧ ((¬ 𝜓𝜑) ∨ (𝜏𝜂)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  if-wif 1011
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 197  df-or 385  df-an 386  df-ifp 1012
This theorem is referenced by:  ifpim1g  37327  ifpbi1b  37329  ifpimimb  37330  ifpor123g  37334  ifpimim  37335
  Copyright terms: Public domain W3C validator