Theorem 3netr4d 2859

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 2849	. 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
4		3netr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	neeqtrrd 2856	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  infpssrlem4  9011  modsumfzodifsn  12605  mgm2nsgrplem4  17231  pmtr3ncomlem1  17716  isdrng2  18580  prmirredlem  19660  uvcf1  19950  dfac14lem  21230  i1fmullem  23267  fta1glem1  23729  fta1blem  23732  plydivlem4  23855  fta1lem  23866  cubic  24376  asinlem  24395  dchrn0  24775  lgsne0  24860  perpneq  25409  axlowdimlem14  25635  cntnevol  29618  subfacp1lem5  30420  nofulllem4  31104  fvtransport  31309  poimirlem1  32580  poimirlem6  32585  poimirlem7  32586  dalem4  33969  cdleme35sn2aw  34764  cdleme39n  34772  cdleme41fva11  34783  trlcone  35034  hdmap1neglem1N  36135  hdmaprnlem3N  36160  stoweidlem23  38916  2zrngnmlid  41739  2zrngnmrid  41740  zlmodzxznm  42080