# Metamath Proof Explorer

## 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 ${⊢}{\phi }$
abnotbtaxb.2 ${⊢}¬{\psi }$
Assertion abnotbtaxb ${⊢}\left({\phi }⊻{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 abnotbtaxb.1 ${⊢}{\phi }$
2 abnotbtaxb.2 ${⊢}¬{\psi }$
3 xor3 ${⊢}¬\left({\phi }↔{\psi }\right)↔\left({\phi }↔¬{\psi }\right)$
4 pm5.1 ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to \left({\phi }↔¬{\psi }\right)$
5 ibibr ${⊢}\left(\left({\phi }\wedge ¬{\psi }\right)\to \left({\phi }↔¬{\psi }\right)\right)↔\left(\left({\phi }\wedge ¬{\psi }\right)\to \left(\left({\phi }↔¬{\psi }\right)↔\left({\phi }\wedge ¬{\psi }\right)\right)\right)$
6 4 5 mpbi ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to \left(\left({\phi }↔¬{\psi }\right)↔\left({\phi }\wedge ¬{\psi }\right)\right)$
7 1 2 6 mp2an ${⊢}\left({\phi }↔¬{\psi }\right)↔\left({\phi }\wedge ¬{\psi }\right)$
8 3 7 bitri ${⊢}¬\left({\phi }↔{\psi }\right)↔\left({\phi }\wedge ¬{\psi }\right)$
9 1 2 8 mpbir2an ${⊢}¬\left({\phi }↔{\psi }\right)$
10 df-xor ${⊢}\left({\phi }⊻{\psi }\right)↔¬\left({\phi }↔{\psi }\right)$
11 9 10 mpbir ${⊢}\left({\phi }⊻{\psi }\right)$