Theorem 3netr4d 3012

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

Hypotheses

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

Assertion

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

Proof of Theorem 3netr4d

Step	Hyp	Ref	Expression
1		3netr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3netr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
3	1, 2	eqnetrd 3002	. 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
4		3netr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	neeqtrrd 3009	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  f1ounsn  7223  infpssrlem4  10226  modsumfzodifsn  13904  mgm2nsgrplem4  18890  pmtr3ncomlem1  19446  isdrng2  20722  prmirredlem  21454  uvcf1  21774  dfac14lem  23607  i1fmullem  25686  fta1glem1  26158  fta1blem  26161  plydivlem4  26287  fta1lem  26298  cubic  26838  asinlem  26857  dchrn0  27238  lgsne0  27323  noextenddif  27657  noresle  27686  perpneq  28807  axlowdimlem14  29049  preimane  32768  cycpmco2lem6  33219  cycpmrn  33231  ricnzr1  33376  psrnzr  33703  mplmulmvr  33730  irngnminplynz  33903  cntnevol  34419  subfacp1lem5  35419  fvtransport  36267  mh-inf3f1  36776  poimirlem1  37995  poimirlem6  38000  poimirlem7  38001  dalem4  40164  cdleme35sn2aw  40957  cdleme39n  40965  cdleme41fva11  40976  trlcone  41227  hdmaprnlem3N  42349  sticksstones2  42639  expeq1d  42808  uvcn0  43035  flt0  43094  stoweidlem23  46473  gpg3kgrtriex  48587  gpgprismgr4cycllem7  48599  2zrngnmlid  48753  2zrngnmrid  48754  zlmodzxznm  48995  line2y  49253