Theorem abnotbtaxb

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

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

Proof

Step	Hyp	Ref	Expression
1		abnotbtaxb.1	⊢ 𝜑
2		abnotbtaxb.2	⊢ ¬ 𝜓
3		xor3	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) )
4		pm5.1	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( 𝜑 ↔ ¬ 𝜓 ) )
5		ibibr	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) → ( 𝜑 ↔ ¬ 𝜓 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜑 ↔ ¬ 𝜓 ) ↔ ( 𝜑 ∧ ¬ 𝜓 ) ) ) )
6	4 5	mpbi	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜑 ↔ ¬ 𝜓 ) ↔ ( 𝜑 ∧ ¬ 𝜓 ) ) )
7	1 2 6	mp2an	⊢ ( ( 𝜑 ↔ ¬ 𝜓 ) ↔ ( 𝜑 ∧ ¬ 𝜓 ) )
8	3 7	bitri	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ∧ ¬ 𝜓 ) )
9	1 2 8	mpbir2an	⊢ ¬ ( 𝜑 ↔ 𝜓 )
10		df-xor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
11	9 10	mpbir	⊢ ( 𝜑 ⊻ 𝜓 )