Metamath Proof Explorer


Theorem mdandyvrx2

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 mdandyvrx2.1 φ ζ
mdandyvrx2.2 ψ σ
mdandyvrx2.3 χ φ
mdandyvrx2.4 θ ψ
mdandyvrx2.5 τ φ
mdandyvrx2.6 η φ
Assertion mdandyvrx2 χ ζ θ σ τ ζ η ζ

Proof

Step Hyp Ref Expression
1 mdandyvrx2.1 φ ζ
2 mdandyvrx2.2 ψ σ
3 mdandyvrx2.3 χ φ
4 mdandyvrx2.4 θ ψ
5 mdandyvrx2.5 τ φ
6 mdandyvrx2.6 η φ
7 1 3 axorbciffatcxorb χ ζ
8 2 4 axorbciffatcxorb θ σ
9 7 8 pm3.2i χ ζ θ σ
10 1 5 axorbciffatcxorb τ ζ
11 9 10 pm3.2i χ ζ θ σ τ ζ
12 1 6 axorbciffatcxorb η ζ
13 11 12 pm3.2i χ ζ θ σ τ ζ η ζ