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

Metamath Proof Explorer

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 → φ
pm2.61iine.2 ⊢ A = C → φ
pm2.61iine.3 ⊢ B = D → φ
Assertion pm2.61iine ⊢ φ

Proof

Step Hyp Ref Expression
1 pm2.61iine.1 ⊢ A ≠ C ∧ B ≠ D → φ
2 pm2.61iine.2 ⊢ A = C → φ
3 pm2.61iine.3 ⊢ B = D → φ
4 3 adantl ⊢ A ≠ C ∧ B = D → φ
5 4 1 pm2.61dane ⊢ A ≠ C → φ
6 2 5 pm2.61ine ⊢ φ