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

Theorem norass 1534
Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass 1501. Remark: Like alternative denial, joint denial is also commutative, see norcom 1523. (Contributed by RP, 29-Oct-2023.) (Proof shortened by Wolf Lammen, 17-Dec-2023.)
Assertion
Ref Expression
norass ((𝜑𝜒) ↔ (((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))))

Proof of Theorem norass
StepHypRef Expression
1 notbi 322 . 2 ((((𝜑 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 𝜒))) ↔ (¬ ((𝜑 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 𝜒))))
2 norasslem1 1531 . . . 4 (((𝜓𝜑) → 𝜒) ↔ ((𝜓 𝜑) ∨ 𝜒))
3 norasslem1 1531 . . . 4 (((𝜓𝜒) → 𝜑) ↔ ((𝜓 𝜒) ∨ 𝜑))
42, 3bibi12i 343 . . 3 ((((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑)) ↔ (((𝜓 𝜑) ∨ 𝜒) ↔ ((𝜓 𝜒) ∨ 𝜑)))
5 bicom 225 . . . . 5 ((𝜑𝜒) ↔ (𝜒𝜑))
6 norasslem2 1532 . . . . . 6 (𝜓 → (𝜒 ↔ ((𝜓𝜑) → 𝜒)))
7 norasslem2 1532 . . . . . 6 (𝜓 → (𝜑 ↔ ((𝜓𝜒) → 𝜑)))
86, 7bibi12d 349 . . . . 5 (𝜓 → ((𝜒𝜑) ↔ (((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑))))
95, 8syl5bb 286 . . . 4 (𝜓 → ((𝜑𝜒) ↔ (((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑))))
10 impimprbi 827 . . . . 5 ((𝜑𝜒) ↔ ((𝜑𝜒) ↔ (𝜒𝜑)))
11 norasslem3 1533 . . . . . 6 𝜓 → ((𝜑𝜒) ↔ ((𝜓𝜑) → 𝜒)))
12 norasslem3 1533 . . . . . 6 𝜓 → ((𝜒𝜑) ↔ ((𝜓𝜒) → 𝜑)))
1311, 12bibi12d 349 . . . . 5 𝜓 → (((𝜑𝜒) ↔ (𝜒𝜑)) ↔ (((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑))))
1410, 13syl5bb 286 . . . 4 𝜓 → ((𝜑𝜒) ↔ (((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑))))
159, 14pm2.61i 185 . . 3 ((𝜑𝜒) ↔ (((𝜓𝜑) → 𝜒) ↔ ((𝜓𝜒) → 𝜑)))
16 norcom 1523 . . . . 5 ((𝜑 𝜓) ↔ (𝜓 𝜑))
1716orbi1i 911 . . . 4 (((𝜑 𝜓) ∨ 𝜒) ↔ ((𝜓 𝜑) ∨ 𝜒))
18 orcom 867 . . . 4 ((𝜑 ∨ (𝜓 𝜒)) ↔ ((𝜓 𝜒) ∨ 𝜑))
1917, 18bibi12i 343 . . 3 ((((𝜑 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 𝜒))) ↔ (((𝜓 𝜑) ∨ 𝜒) ↔ ((𝜓 𝜒) ∨ 𝜑)))
204, 15, 193bitr4i 306 . 2 ((𝜑𝜒) ↔ (((𝜑 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 𝜒))))
21 df-nor 1522 . . 3 (((𝜑 𝜓) 𝜒) ↔ ¬ ((𝜑 𝜓) ∨ 𝜒))
22 df-nor 1522 . . 3 ((𝜑 (𝜓 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 𝜒)))
2321, 22bibi12i 343 . 2 ((((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))) ↔ (¬ ((𝜑 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 𝜒))))
241, 20, 233bitr4i 306 1 ((𝜑𝜒) ↔ (((𝜑 𝜓) 𝜒) ↔ (𝜑 (𝜓 𝜒))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wo 844   wnor 1521
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 210  df-an 400  df-or 845  df-nor 1522
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator