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 ( 𝜑𝐴𝐵 )
3netr3g.2 𝐴 = 𝐶
3netr3g.3 𝐵 = 𝐷
Assertion 3netr3g ( 𝜑𝐶𝐷 )

Proof

Step Hyp Ref Expression
1 3netr3g.1 ( 𝜑𝐴𝐵 )
2 3netr3g.2 𝐴 = 𝐶
3 3netr3g.3 𝐵 = 𝐷
4 2 3 neeq12i ( 𝐴𝐵𝐶𝐷 )
5 1 4 sylib ( 𝜑𝐶𝐷 )