This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.61da3ne

Description: Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013) (Proof shortened by Wolf Lammen, 25-Nov-2019)

		Ref	Expression
	Hypotheses	pm2.61da3ne.1	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 )
		pm2.61da3ne.2	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 )
		pm2.61da3ne.3	⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝜓 )
		pm2.61da3ne.4	⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ) → 𝜓 )
	Assertion	pm2.61da3ne	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		pm2.61da3ne.1	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 )
2		pm2.61da3ne.2	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 )
3		pm2.61da3ne.3	⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → 𝜓 )
4		pm2.61da3ne.4	⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ) → 𝜓 )
5	1	a1d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) → 𝜓 ) )
6	4	3exp2	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 → ( 𝐶 ≠ 𝐷 → ( 𝐸 ≠ 𝐹 → 𝜓 ) ) ) )
7	6	imp4b	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) → 𝜓 ) )
8	5 7	pm2.61dane	⊢ ( 𝜑 → ( ( 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) → 𝜓 ) )
9	8	imp	⊢ ( ( 𝜑 ∧ ( 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ) → 𝜓 )
10	2 3 9	pm2.61da2ne	⊢ ( 𝜑 → 𝜓 )