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	$⊢ (φ \land A = B) \to ψ$
		pm2.61da3ne.2	$⊢ (φ \land C = D) \to ψ$
		pm2.61da3ne.3	$⊢ (φ \land E = F) \to ψ$
		pm2.61da3ne.4	$⊢ (φ \land (A \neq B \land C \neq D \land E \neq F)) \to ψ$
	Assertion	pm2.61da3ne	$⊢ φ \to ψ$

Proof

Step	Hyp	Ref	Expression
1		pm2.61da3ne.1	$⊢ (φ \land A = B) \to ψ$
2		pm2.61da3ne.2	$⊢ (φ \land C = D) \to ψ$
3		pm2.61da3ne.3	$⊢ (φ \land E = F) \to ψ$
4		pm2.61da3ne.4	$⊢ (φ \land (A \neq B \land C \neq D \land E \neq F)) \to ψ$
5	1	a1d	$⊢ (φ \land A = B) \to ((C \neq D \land E \neq F) \to ψ)$
6	4	3exp2	$⊢ φ \to (A \neq B \to (C \neq D \to (E \neq F \to ψ)))$
7	6	imp4b	$⊢ (φ \land A \neq B) \to ((C \neq D \land E \neq F) \to ψ)$
8	5 7	pm2.61dane	$⊢ φ \to ((C \neq D \land E \neq F) \to ψ)$
9	8	imp	$⊢ (φ \land (C \neq D \land E \neq F)) \to ψ$
10	2 3 9	pm2.61da2ne	$⊢ φ \to ψ$