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 ( ( ( ( 𝜒𝜎 ) ∧ ( 𝜃𝜎 ) ) ∧ ( 𝜏𝜁 ) ) ∧ ( 𝜂𝜁 ) )

Proof

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 ( ( ( ( 𝜒𝜎 ) ∧ ( 𝜃𝜎 ) ) ∧ ( 𝜏𝜁 ) ) ∧ ( 𝜂𝜁 ) )