MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  norassOLD Structured version   Visualization version   GIF version

Theorem norassOLD 1530
Description: Obsolete version of norass 1529 as of 17-Dec-2023. (Contributed by RP, 29-Oct-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
norassOLD ((𝜑𝜒) ↔ (((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))))

Proof of Theorem norassOLD
StepHypRef Expression
1 id 22 . . . . . 6 ((𝜑𝜒) → (𝜑𝜒))
21notbid 320 . . . . 5 ((𝜑𝜒) → (¬ 𝜑 ↔ ¬ 𝜒))
32bicomd 225 . . . 4 ((𝜑𝜒) → (¬ 𝜒 ↔ ¬ 𝜑))
42anbi2d 630 . . . . 5 ((𝜑𝜒) → ((¬ 𝜓 ∧ ¬ 𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜒)))
54notbid 320 . . . 4 ((𝜑𝜒) → (¬ (¬ 𝜓 ∧ ¬ 𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
63, 5anbi12d 632 . . 3 ((𝜑𝜒) → ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
7 olc 864 . . . . . . . . . . 11 (𝜑 → (𝜓𝜑))
8 oran 986 . . . . . . . . . . 11 ((𝜓𝜑) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
97, 8sylib 220 . . . . . . . . . 10 (𝜑 → ¬ (¬ 𝜓 ∧ ¬ 𝜑))
109anim1ci 617 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝜒) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
11 animorl 974 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝜒) → (𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)))
12 oran 986 . . . . . . . . . 10 ((𝜑 ∨ (¬ 𝜓 ∧ ¬ 𝜒)) ↔ ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
1311, 12sylib 220 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝜒) → ¬ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
1410, 13jcnd 165 . . . . . . . 8 ((𝜑 ∧ ¬ 𝜒) → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
1514ex 415 . . . . . . 7 (𝜑 → (¬ 𝜒 → ¬ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))))
1615con4d 115 . . . . . 6 (𝜑 → (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → 𝜒))
1716com12 32 . . . . 5 (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑𝜒))
18 olc 864 . . . . . . . . . . 11 (𝜒 → (𝜓𝜒))
19 oran 986 . . . . . . . . . . 11 ((𝜓𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
2018, 19sylib 220 . . . . . . . . . 10 (𝜒 → ¬ (¬ 𝜓 ∧ ¬ 𝜒))
2120anim1ci 617 . . . . . . . . 9 ((𝜒 ∧ ¬ 𝜑) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
22 animorl 974 . . . . . . . . . 10 ((𝜒 ∧ ¬ 𝜑) → (𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)))
23 oran 986 . . . . . . . . . 10 ((𝜒 ∨ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
2422, 23sylib 220 . . . . . . . . 9 ((𝜒 ∧ ¬ 𝜑) → ¬ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
2521, 24jcnd 165 . . . . . . . 8 ((𝜒 ∧ ¬ 𝜑) → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))))
2625ex 415 . . . . . . 7 (𝜒 → (¬ 𝜑 → ¬ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
2726con4d 115 . . . . . 6 (𝜒 → (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → 𝜑))
2827com12 32 . . . . 5 (((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑))) → (𝜒𝜑))
2917, 28anim12i 614 . . . 4 ((((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))) → ((𝜑𝜒) ∧ (𝜒𝜑)))
30 dfbi2 477 . . . 4 (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ↔ (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) → (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) ∧ ((¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)) → (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))))
31 dfbi2 477 . . . 4 ((𝜑𝜒) ↔ ((𝜑𝜒) ∧ (𝜒𝜑)))
3229, 30, 313imtr4i 294 . . 3 (((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))) → (𝜑𝜒))
336, 32impbii 211 . 2 ((𝜑𝜒) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
34 norcom 1519 . . . 4 (((𝜑 𝜓) 𝜒) ↔ (𝜒 (𝜑 𝜓)))
35 df-nor 1518 . . . 4 ((𝜒 (𝜑 𝜓)) ↔ ¬ (𝜒 ∨ (𝜑 𝜓)))
36 ioran 980 . . . . 5 (¬ (𝜒 ∨ (𝜑 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (𝜑 𝜓)))
37 norcom 1519 . . . . . . . 8 ((𝜑 𝜓) ↔ (𝜓 𝜑))
38 df-nor 1518 . . . . . . . 8 ((𝜓 𝜑) ↔ ¬ (𝜓𝜑))
39 ioran 980 . . . . . . . 8 (¬ (𝜓𝜑) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
4037, 38, 393bitri 299 . . . . . . 7 ((𝜑 𝜓) ↔ (¬ 𝜓 ∧ ¬ 𝜑))
4140notbii 322 . . . . . 6 (¬ (𝜑 𝜓) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜑))
4241anbi2i 624 . . . . 5 ((¬ 𝜒 ∧ ¬ (𝜑 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
4336, 42bitri 277 . . . 4 (¬ (𝜒 ∨ (𝜑 𝜓)) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
4434, 35, 433bitri 299 . . 3 (((𝜑 𝜓) 𝜒) ↔ (¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)))
45 df-nor 1518 . . . 4 ((𝜑 (𝜓 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 𝜒)))
46 ioran 980 . . . 4 (¬ (𝜑 ∨ (𝜓 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (𝜓 𝜒)))
47 df-nor 1518 . . . . . . 7 ((𝜓 𝜒) ↔ ¬ (𝜓𝜒))
48 ioran 980 . . . . . . 7 (¬ (𝜓𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
4947, 48bitri 277 . . . . . 6 ((𝜓 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
5049notbii 322 . . . . 5 (¬ (𝜓 𝜒) ↔ ¬ (¬ 𝜓 ∧ ¬ 𝜒))
5150anbi2i 624 . . . 4 ((¬ 𝜑 ∧ ¬ (𝜓 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
5245, 46, 513bitri 299 . . 3 ((𝜑 (𝜓 𝜒)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒)))
5344, 52bibi12i 342 . 2 ((((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))) ↔ ((¬ 𝜒 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜑)) ↔ (¬ 𝜑 ∧ ¬ (¬ 𝜓 ∧ ¬ 𝜒))))
5433, 53bitr4i 280 1 ((𝜑𝜒) ↔ (((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   wnor 1517
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 209  df-an 399  df-or 844  df-nor 1518
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator