Theorem 3netr4d 3059

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

Syntax hints:   → wi 4   = wceq 1520   ≠ wne 2982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-ne 2983

This theorem is referenced by:  infpssrlem4  9563  modsumfzodifsn  13150  mgm2nsgrplem4  17835  pmtr3ncomlem1  18320  isdrng2  19190  prmirredlem  20310  uvcf1  20606  dfac14lem  21897  i1fmullem  23966  fta1glem1  24430  fta1blem  24433  plydivlem4  24556  fta1lem  24567  cubic  25096  asinlem  25115  dchrn0  25496  lgsne0  25581  perpneq  26170  axlowdimlem14  26412  preimane  30078  cntnevol  31060  subfacp1lem5  31995  noextenddif  32729  noresle  32754  fvtransport  33047  poimirlem1  34370  poimirlem6  34375  poimirlem7  34376  dalem4  36282  cdleme35sn2aw  37075  cdleme39n  37083  cdleme41fva11  37094  trlcone  37345  hdmaprnlem3N  38467  uvcn0  38628  stoweidlem23  41804  2zrngnmlid  43652  2zrngnmrid  43653  zlmodzxznm  43986  line2y  44177