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


Step Hyp Ref Expression
1 mdandyvrx3.1 φ ζ
2 mdandyvrx3.2 ψ σ
3 mdandyvrx3.3 χ ψ
4 mdandyvrx3.4 θ ψ
5 mdandyvrx3.5 τ φ
6 mdandyvrx3.6 η φ
7 2 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 χ σ θ σ τ ζ η ζ