# Metamath Proof Explorer

## Theorem mdandyvrx3

Description: Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016)

Ref Expression
Hypotheses mdandyvrx3.1 ${⊢}\left({\phi }⊻{\zeta }\right)$
mdandyvrx3.2 ${⊢}\left({\psi }⊻{\sigma }\right)$
mdandyvrx3.3 ${⊢}{\chi }↔{\psi }$
mdandyvrx3.4 ${⊢}{\theta }↔{\psi }$
mdandyvrx3.5 ${⊢}{\tau }↔{\phi }$
mdandyvrx3.6 ${⊢}{\eta }↔{\phi }$
Assertion mdandyvrx3 ${⊢}\left(\left(\left(\left({\chi }⊻{\sigma }\right)\wedge \left({\theta }⊻{\sigma }\right)\right)\wedge \left({\tau }⊻{\zeta }\right)\right)\wedge \left({\eta }⊻{\zeta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 mdandyvrx3.1 ${⊢}\left({\phi }⊻{\zeta }\right)$
2 mdandyvrx3.2 ${⊢}\left({\psi }⊻{\sigma }\right)$
3 mdandyvrx3.3 ${⊢}{\chi }↔{\psi }$
4 mdandyvrx3.4 ${⊢}{\theta }↔{\psi }$
5 mdandyvrx3.5 ${⊢}{\tau }↔{\phi }$
6 mdandyvrx3.6 ${⊢}{\eta }↔{\phi }$
7 2 3 axorbciffatcxorb ${⊢}\left({\chi }⊻{\sigma }\right)$
8 2 4 axorbciffatcxorb ${⊢}\left({\theta }⊻{\sigma }\right)$
9 7 8 pm3.2i ${⊢}\left(\left({\chi }⊻{\sigma }\right)\wedge \left({\theta }⊻{\sigma }\right)\right)$
10 1 5 axorbciffatcxorb ${⊢}\left({\tau }⊻{\zeta }\right)$
11 9 10 pm3.2i ${⊢}\left(\left(\left({\chi }⊻{\sigma }\right)\wedge \left({\theta }⊻{\sigma }\right)\right)\wedge \left({\tau }⊻{\zeta }\right)\right)$
12 1 6 axorbciffatcxorb ${⊢}\left({\eta }⊻{\zeta }\right)$
13 11 12 pm3.2i ${⊢}\left(\left(\left(\left({\chi }⊻{\sigma }\right)\wedge \left({\theta }⊻{\sigma }\right)\right)\wedge \left({\tau }⊻{\zeta }\right)\right)\wedge \left({\eta }⊻{\zeta }\right)\right)$