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

Metamath Proof Explorer

Theorem 3netr3g

Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012)

Ref Expression
Hypotheses 3netr3g.1 ⊢ φ → A ≠ B
3netr3g.2 ⊢ A = C
3netr3g.3 ⊢ B = D
Assertion 3netr3g ⊢ φ → C ≠ D

Proof

Step Hyp Ref Expression
1 3netr3g.1 ⊢ φ → A ≠ B
2 3netr3g.2 ⊢ A = C
3 3netr3g.3 ⊢ B = D
4 2 3 neeq12i ⊢ A ≠ B ↔ C ≠ D
5 1 4 sylib ⊢ φ → C ≠ D