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	|- ( ( A =/= C /\ B =/= D ) -> ph )
	pm2.61iine.2	|- ( A = C -> ph )
	pm2.61iine.3	|- ( B = D -> ph )
Assertion	pm2.61iine	|- ph

Proof

Step	Hyp	Ref	Expression
1		pm2.61iine.1	|- ( ( A =/= C /\ B =/= D ) -> ph )
2		pm2.61iine.2	|- ( A = C -> ph )
3		pm2.61iine.3	|- ( B = D -> ph )
4	3	adantl	|- ( ( A =/= C /\ B = D ) -> ph )
5	4 1	pm2.61dane	|- ( A =/= C -> ph )
6	2 5	pm2.61ine	|- ph