Theorem 3netr3d 3004

Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypotheses

Ref	Expression
3netr3d.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
3netr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3netr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3netr3d	⊢ (𝜑 → 𝐶 ≠ 𝐷)

Proof of Theorem 3netr3d

Step	Hyp	Ref	Expression
1		3netr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3netr3d.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
3		3netr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	neeqtrd 2997	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
5	1, 4	eqnetrrd 2996	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  subrgnzr  20507  clmopfne  25021  dchrisum0re  27449  fracfld  33269  qsnzr  33415  dimlssid  33640  algextdeglem4  33728  constrrtll  33739  cdlemg9a  40670  cdlemg11aq  40676  cdlemg12b  40682  cdlemg12  40688  cdlemg13  40690  cdlemg19  40722  cdlemk3  40871  cdlemk12  40888  cdlemk12u  40910  lclkrlem2g  41551  mapdncol  41708  mapdpglem29  41738  hdmaprnlem1N  41887  hdmap14lem9  41914  aks6d1c2p2  42151  ricdrng1  42560  pellex  42867