Description: A symmetry with -/\ .
See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | nandsym1 |
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 |