Metamath Proof Explorer


Theorem mdandyvrx6

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 mdandyvrx6.1 ( 𝜑𝜁 )
mdandyvrx6.2 ( 𝜓𝜎 )
mdandyvrx6.3 ( 𝜒𝜑 )
mdandyvrx6.4 ( 𝜃𝜓 )
mdandyvrx6.5 ( 𝜏𝜓 )
mdandyvrx6.6 ( 𝜂𝜑 )
Assertion mdandyvrx6 ( ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜎 ) ) ∧ ( 𝜏𝜎 ) ) ∧ ( 𝜂𝜁 ) )

Proof

Step Hyp Ref Expression
1 mdandyvrx6.1 ( 𝜑𝜁 )
2 mdandyvrx6.2 ( 𝜓𝜎 )
3 mdandyvrx6.3 ( 𝜒𝜑 )
4 mdandyvrx6.4 ( 𝜃𝜓 )
5 mdandyvrx6.5 ( 𝜏𝜓 )
6 mdandyvrx6.6 ( 𝜂𝜑 )
7 1 3 axorbciffatcxorb ( 𝜒𝜁 )
8 2 4 axorbciffatcxorb ( 𝜃𝜎 )
9 7 8 pm3.2i ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜎 ) )
10 2 5 axorbciffatcxorb ( 𝜏𝜎 )
11 9 10 pm3.2i ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜎 ) ) ∧ ( 𝜏𝜎 ) )
12 1 6 axorbciffatcxorb ( 𝜂𝜁 )
13 11 12 pm3.2i ( ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜎 ) ) ∧ ( 𝜏𝜎 ) ) ∧ ( 𝜂𝜁 ) )