Metamath Proof Explorer


Theorem nandsym1

Description: A symmetry with -/\ .

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

Ref Expression
Assertion nandsym1 ψ ψ ψ φ

Proof

Step Hyp Ref Expression
1 df-nan ψ ψ ¬ ψ ψ
2 1 biimpi ψ ψ ¬ ψ ψ
3 df-nan ψ ¬ ψ
4 3 anbi2i ψ ψ ψ ¬ ψ
5 2 4 sylnib ψ ψ ¬ ψ ¬ ψ
6 simpl ψ φ ψ
7 fal ¬
8 7 intnan ¬ ψ
9 6 8 jctir ψ φ ψ ¬ ψ
10 5 9 nsyl ψ ψ ¬ ψ φ
11 df-nan ψ φ ¬ ψ φ
12 10 11 sylibr ψ ψ ψ φ