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	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) → 𝜑 )
	pm2.61iine.2	⊢ ( 𝐴 = 𝐶 → 𝜑 )
	pm2.61iine.3	⊢ ( 𝐵 = 𝐷 → 𝜑 )
Assertion	pm2.61iine	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		pm2.61iine.1	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) → 𝜑 )
2		pm2.61iine.2	⊢ ( 𝐴 = 𝐶 → 𝜑 )
3		pm2.61iine.3	⊢ ( 𝐵 = 𝐷 → 𝜑 )
4	3	adantl	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 = 𝐷 ) → 𝜑 )
5	4 1	pm2.61dane	⊢ ( 𝐴 ≠ 𝐶 → 𝜑 )
6	2 5	pm2.61ine	⊢ 𝜑