Theorem pm2.61iine

Description: Equality version of pm2.61ii . (Contributed by Scott Fenton, 13-Jun-2013) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Hypotheses	pm2.61iine.1	$$⊢\left(A\ne C\wedge B\ne D\right)\to \phi$$
	pm2.61iine.2	$$⊢A=C\to \phi$$
	pm2.61iine.3	$$⊢B=D\to \phi$$
Assertion	pm2.61iine	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.61iine.1	$$⊢\left(A\ne C\wedge B\ne D\right)\to \phi$$
2		pm2.61iine.2	$$⊢A=C\to \phi$$
3		pm2.61iine.3	$$⊢B=D\to \phi$$
4	3	adantl	$$⊢\left(A\ne C\wedge B=D\right)\to \phi$$
5	4 1	pm2.61dane	$$⊢A\ne C\to \phi$$
6	2 5	pm2.61ine	$$⊢\phi$$