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	|- ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )

Proof of Theorem rp-fakenanass

Step	Hyp	Ref	Expression
1		bicom1 211	. . . 4 |- ( ( ph <-> ch ) -> ( ch <-> ph ) )
2		nanbi2 1456	. . . 4 |- ( ( ph <-> ch ) -> ( ( ps -/\ ph ) <-> ( ps -/\ ch ) ) )
3	1, 2	nanbi12d 1463	. . 3 |- ( ( ph <-> ch ) -> ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
4		nannan 1451	. . . . . 6 |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
5		simpr 477	. . . . . . 7 |- ( ( ps /\ ch ) -> ch )
6	5	imim2i 16	. . . . . 6 |- ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ch ) )
7	4, 6	sylbi 207	. . . . 5 |- ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph -> ch ) )
8		nannan 1451	. . . . . 6 |- ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ch -> ( ps /\ ph ) ) )
9		simpr 477	. . . . . . 7 |- ( ( ps /\ ph ) -> ph )
10	9	imim2i 16	. . . . . 6 |- ( ( ch -> ( ps /\ ph ) ) -> ( ch -> ph ) )
11	8, 10	sylbi 207	. . . . 5 |- ( ( ch -/\ ( ps -/\ ph ) ) -> ( ch -> ph ) )
12	7, 11	impbid21d 201	. . . 4 |- ( ( ch -/\ ( ps -/\ ph ) ) -> ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph <-> ch ) ) )
13	8	notbii 310	. . . . . . 7 |- ( -. ( ch -/\ ( ps -/\ ph ) ) <-> -. ( ch -> ( ps /\ ph ) ) )
14		pm4.61 442	. . . . . . 7 |- ( -. ( ch -> ( ps /\ ph ) ) <-> ( ch /\ -. ( ps /\ ph ) ) )
15		ianor 509	. . . . . . . 8 |- ( -. ( ps /\ ph ) <-> ( -. ps \/ -. ph ) )
16	15	anbi2i 730	. . . . . . 7 |- ( ( ch /\ -. ( ps /\ ph ) ) <-> ( ch /\ ( -. ps \/ -. ph ) ) )
17	13, 14, 16	3bitri 286	. . . . . 6 |- ( -. ( ch -/\ ( ps -/\ ph ) ) <-> ( ch /\ ( -. ps \/ -. ph ) ) )
18	4	notbii 310	. . . . . . 7 |- ( -. ( ph -/\ ( ps -/\ ch ) ) <-> -. ( ph -> ( ps /\ ch ) ) )
19		pm4.61 442	. . . . . . 7 |- ( -. ( ph -> ( ps /\ ch ) ) <-> ( ph /\ -. ( ps /\ ch ) ) )
20		ianor 509	. . . . . . . 8 |- ( -. ( ps /\ ch ) <-> ( -. ps \/ -. ch ) )
21	20	anbi2i 730	. . . . . . 7 |- ( ( ph /\ -. ( ps /\ ch ) ) <-> ( ph /\ ( -. ps \/ -. ch ) ) )
22	18, 19, 21	3bitri 286	. . . . . 6 |- ( -. ( ph -/\ ( ps -/\ ch ) ) <-> ( ph /\ ( -. ps \/ -. ch ) ) )
23		pm5.1 902	. . . . . . . 8 |- ( ( ph /\ ch ) -> ( ph <-> ch ) )
24	23	ancoms 469	. . . . . . 7 |- ( ( ch /\ ph ) -> ( ph <-> ch ) )
25	24	ad2ant2r 783	. . . . . 6 |- ( ( ( ch /\ ( -. ps \/ -. ph ) ) /\ ( ph /\ ( -. ps \/ -. ch ) ) ) -> ( ph <-> ch ) )
26	17, 22, 25	syl2anb 496	. . . . 5 |- ( ( -. ( ch -/\ ( ps -/\ ph ) ) /\ -. ( ph -/\ ( ps -/\ ch ) ) ) -> ( ph <-> ch ) )
27	26	ex 450	. . . 4 |- ( -. ( ch -/\ ( ps -/\ ph ) ) -> ( -. ( ph -/\ ( ps -/\ ch ) ) -> ( ph <-> ch ) ) )
28	12, 27	bija 370	. . 3 |- ( ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) -> ( ph <-> ch ) )
29	3, 28	impbii 199	. 2 |- ( ( ph <-> ch ) <-> ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
30		nancom 1450	. . . . 5 |- ( ( ps -/\ ph ) <-> ( ph -/\ ps ) )
31	30	nanbi2i 1459	. . . 4 |- ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ch -/\ ( ph -/\ ps ) ) )
32		nancom 1450	. . . 4 |- ( ( ch -/\ ( ph -/\ ps ) ) <-> ( ( ph -/\ ps ) -/\ ch ) )
33	31, 32	bitri 264	. . 3 |- ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ( ph -/\ ps ) -/\ ch ) )
34	33	bibi1i 328	. 2 |- ( ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
35	29, 34	bitri 264	1 |- ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )

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)