Theorem nandsym1

Description: A symmetry with -/\ .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		df-nan	|- ( ( ps -/\ ( ps -/\ F. ) ) <-> -. ( ps /\ ( ps -/\ F. ) ) )
2	1	biimpi	|- ( ( ps -/\ ( ps -/\ F. ) ) -> -. ( ps /\ ( ps -/\ F. ) ) )
3		df-nan	|- ( ( ps -/\ F. ) <-> -. ( ps /\ F. ) )
4	3	anbi2i	|- ( ( ps /\ ( ps -/\ F. ) ) <-> ( ps /\ -. ( ps /\ F. ) ) )
5	2 4	sylnib	|- ( ( ps -/\ ( ps -/\ F. ) ) -> -. ( ps /\ -. ( ps /\ F. ) ) )
6		simpl	|- ( ( ps /\ ph ) -> ps )
7		fal	|- -. F.
8	7	intnan	|- -. ( ps /\ F. )
9	6 8	jctir	|- ( ( ps /\ ph ) -> ( ps /\ -. ( ps /\ F. ) ) )
10	5 9	nsyl	|- ( ( ps -/\ ( ps -/\ F. ) ) -> -. ( ps /\ ph ) )
11		df-nan	|- ( ( ps -/\ ph ) <-> -. ( ps /\ ph ) )
12	10 11	sylibr	|- ( ( ps -/\ ( ps -/\ F. ) ) -> ( ps -/\ ph ) )