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	⊢ ( ( 𝜓 ⊼ ( 𝜓 ⊼ ⊥ ) ) → ( 𝜓 ⊼ 𝜑 ) )