Theorem rp-fakenanass 36879

Description: A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)

Assertion

Ref	Expression
rp-fakenanass	⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

Proof of Theorem rp-fakenanass

Step	Hyp	Ref	Expression
1		bicom1 210	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (𝜒 ↔ 𝜑))
2		nanbi2 1448	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → ((𝜓 ⊼ 𝜑) ↔ (𝜓 ⊼ 𝜒)))
3	1, 2	nanbi12d 1455	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
4		nannan 1443	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
5		simpr 476	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	imim2i 16	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
7	4, 6	sylbi 206	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → 𝜒))
8		nannan 1443	. . . . . 6 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 → (𝜓 ∧ 𝜑)))
9		simpr 476	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
10	9	imim2i 16	. . . . . 6 ⊢ ((𝜒 → (𝜓 ∧ 𝜑)) → (𝜒 → 𝜑))
11	8, 10	sylbi 206	. . . . 5 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (𝜒 → 𝜑))
12	7, 11	impbid21d 200	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
13	8	notbii 309	. . . . . . 7 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ¬ (𝜒 → (𝜓 ∧ 𝜑)))
14		pm4.61 441	. . . . . . 7 ⊢ (¬ (𝜒 → (𝜓 ∧ 𝜑)) ↔ (𝜒 ∧ ¬ (𝜓 ∧ 𝜑)))
15		ianor 508	. . . . . . . 8 ⊢ (¬ (𝜓 ∧ 𝜑) ↔ (¬ 𝜓 ∨ ¬ 𝜑))
16	15	anbi2i 726	. . . . . . 7 ⊢ ((𝜒 ∧ ¬ (𝜓 ∧ 𝜑)) ↔ (𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)))
17	13, 14, 16	3bitri 285	. . . . . 6 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)))
18	4	notbii 309	. . . . . . 7 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ ¬ (𝜑 → (𝜓 ∧ 𝜒)))
19		pm4.61 441	. . . . . . 7 ⊢ (¬ (𝜑 → (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ ¬ (𝜓 ∧ 𝜒)))
20		ianor 508	. . . . . . . 8 ⊢ (¬ (𝜓 ∧ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒))
21	20	anbi2i 726	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒)))
22	18, 19, 21	3bitri 285	. . . . . 6 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒)))
23		pm5.1 898	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ↔ 𝜒))
24	23	ancoms 468	. . . . . . 7 ⊢ ((𝜒 ∧ 𝜑) → (𝜑 ↔ 𝜒))
25	24	ad2ant2r 779	. . . . . 6 ⊢ (((𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)) ∧ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒))) → (𝜑 ↔ 𝜒))
26	17, 22, 25	syl2anb 495	. . . . 5 ⊢ ((¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ∧ ¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
27	26	ex 449	. . . 4 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
28	12, 27	bija 369	. . 3 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
29	3, 28	impbii 198	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
30		nancom 1442	. . . . 5 ⊢ ((𝜓 ⊼ 𝜑) ↔ (𝜑 ⊼ 𝜓))
31	30	nanbi2i 1451	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ⊼ (𝜑 ⊼ 𝜓)))
32		nancom 1442	. . . 4 ⊢ ((𝜒 ⊼ (𝜑 ⊼ 𝜓)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
33	31, 32	bitri 263	. . 3 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
34	33	bibi1i 327	. 2 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
35	29, 34	bitri 263	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ⊼ wnan 1439

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 196  df-or 384  df-an 385  df-nan 1440

This theorem is referenced by: (None)