Metamath Proof Explorer

Theorem 3netr4g

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

Ref Expression
Hypotheses 3netr4g.1 φ A B
3netr4g.2 C = A
3netr4g.3 D = B
Assertion 3netr4g φ C D


Step Hyp Ref Expression
1 3netr4g.1 φ A B
2 3netr4g.2 C = A
3 3netr4g.3 D = B
4 2 3 neeq12i C D A B
5 1 4 sylibr φ C D