Theorem abnotataxb

Description: Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016)

	Ref	Expression
Hypotheses	abnotataxb.1	⊢ ¬ 𝜑
	abnotataxb.2	⊢ 𝜓
Assertion	abnotataxb	⊢ ( 𝜑 ⊻ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		abnotataxb.1	⊢ ¬ 𝜑
2		abnotataxb.2	⊢ 𝜓
3	2 1	pm3.2i	⊢ ( 𝜓 ∧ ¬ 𝜑 )
4	3	olci	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) )
5		xor	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) )
6	4 5	mpbir	⊢ ¬ ( 𝜑 ↔ 𝜓 )
7		df-xor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
8	6 7	mpbir	⊢ ( 𝜑 ⊻ 𝜓 )