Theorem nandsym1 14246

Description: A symmetry with -/\.

See negsym1 14241 for more information.

Assertion

Ref	Expression
nandsym1	|- ((ps -/\ (ps -/\ F. )) -> (ps -/\ ph))

Proof of Theorem nandsym1

Step	Hyp	Ref	Expression
1		df-nand 1230	. . . 4 |- ((ps -/\ (ps -/\ F. )) <-> -. (ps /\ (ps -/\ F. )))
2	1	biimpi 168	. . 3 |- ((ps -/\ (ps -/\ F. )) -> -. (ps /\ (ps -/\ F. )))
3		df-nand 1230	. . . . 5 |- ((ps -/\ F. ) <-> -. (ps /\ F. ))
4	3	anbi2i 538	. . . 4 |- ((ps /\ (ps -/\ F. )) <-> (ps /\ -. (ps /\ F. )))
5	4	biimpri 169	. . 3 |- ((ps /\ -. (ps /\ F. )) -> (ps /\ (ps -/\ F. )))
6	2, 5	nsyl 131	. 2 |- ((ps -/\ (ps -/\ F. )) -> -. (ps /\ -. (ps /\ F. )))
7		simpl 346	. . . 4 |- ((ps /\ ph) -> ps)
8		notfal 1265	. . . . 5 |- -. F.
9	8	intnan 755	. . . 4 |- -. (ps /\ F. )
10	7, 9	jctir 317	. . 3 |- ((ps /\ ph) -> (ps /\ -. (ps /\ F. )))
11	10	con3i 114	. 2 |- (-. (ps /\ -. (ps /\ F. )) -> -. (ps /\ ph))
12		df-nand 1230	. . 3 |- ((ps -/\ ph) <-> -. (ps /\ ph))
13	12	biimpri 169	. 2 |- (-. (ps /\ ph) -> (ps -/\ ph))
14	6, 11, 13	3syl 24	1 |- ((ps -/\ (ps -/\ F. )) -> (ps -/\ ph))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   -/\ wnand 1229   F. wfal 1261

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-nand 1230  df-tru 1262  df-fal 1263

Copyright terms: Public domain