Theorem rp-fakenanass 37860

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 211	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (𝜒 ↔ 𝜑))
2		nanbi2 1456	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → ((𝜓 ⊼ 𝜑) ↔ (𝜓 ⊼ 𝜒)))
3	1, 2	nanbi12d 1463	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
4		nannan 1451	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
5		simpr 477	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	imim2i 16	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
7	4, 6	sylbi 207	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → 𝜒))
8		nannan 1451	. . . . . 6 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 → (𝜓 ∧ 𝜑)))
9		simpr 477	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
10	9	imim2i 16	. . . . . 6 ⊢ ((𝜒 → (𝜓 ∧ 𝜑)) → (𝜒 → 𝜑))
11	8, 10	sylbi 207	. . . . 5 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (𝜒 → 𝜑))
12	7, 11	impbid21d 201	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
13	8	notbii 310	. . . . . . 7 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ¬ (𝜒 → (𝜓 ∧ 𝜑)))
14		pm4.61 442	. . . . . . 7 ⊢ (¬ (𝜒 → (𝜓 ∧ 𝜑)) ↔ (𝜒 ∧ ¬ (𝜓 ∧ 𝜑)))
15		ianor 509	. . . . . . . 8 ⊢ (¬ (𝜓 ∧ 𝜑) ↔ (¬ 𝜓 ∨ ¬ 𝜑))
16	15	anbi2i 730	. . . . . . 7 ⊢ ((𝜒 ∧ ¬ (𝜓 ∧ 𝜑)) ↔ (𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)))
17	13, 14, 16	3bitri 286	. . . . . 6 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)))
18	4	notbii 310	. . . . . . 7 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ ¬ (𝜑 → (𝜓 ∧ 𝜒)))
19		pm4.61 442	. . . . . . 7 ⊢ (¬ (𝜑 → (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ ¬ (𝜓 ∧ 𝜒)))
20		ianor 509	. . . . . . . 8 ⊢ (¬ (𝜓 ∧ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒))
21	20	anbi2i 730	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒)))
22	18, 19, 21	3bitri 286	. . . . . 6 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒)))
23		pm5.1 902	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ↔ 𝜒))
24	23	ancoms 469	. . . . . . 7 ⊢ ((𝜒 ∧ 𝜑) → (𝜑 ↔ 𝜒))
25	24	ad2ant2r 783	. . . . . 6 ⊢ (((𝜒 ∧ (¬ 𝜓 ∨ ¬ 𝜑)) ∧ (𝜑 ∧ (¬ 𝜓 ∨ ¬ 𝜒))) → (𝜑 ↔ 𝜒))
26	17, 22, 25	syl2anb 496	. . . . 5 ⊢ ((¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) ∧ ¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
27	26	ex 450	. . . 4 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
28	12, 27	bija 370	. . 3 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
29	3, 28	impbii 199	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
30		nancom 1450	. . . . 5 ⊢ ((𝜓 ⊼ 𝜑) ↔ (𝜑 ⊼ 𝜓))
31	30	nanbi2i 1459	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ⊼ (𝜑 ⊼ 𝜓)))
32		nancom 1450	. . . 4 ⊢ ((𝜒 ⊼ (𝜑 ⊼ 𝜓)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
33	31, 32	bitri 264	. . 3 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
34	33	bibi1i 328	. 2 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
35	29, 34	bitri 264	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ⊼ wnan 1447

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-nan 1448

This theorem is referenced by: (None)