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 ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) → 𝜑 )
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 ⊢ 𝜑