Theorem 3netr4d 2871

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	|- ( ph -> A =/= B )
3netr4d.2	|- ( ph -> C = A )
3netr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3netr4d	|- ( ph -> C =/= D )

Proof of Theorem 3netr4d

Step	Hyp	Ref	Expression
1		3netr4d.2	. . 3 |- ( ph -> C = A )
2		3netr4d.1	. . 3 |- ( ph -> A =/= B )
3	1, 2	eqnetrd 2861	. 2 |- ( ph -> C =/= B )
4		3netr4d.3	. 2 |- ( ph -> D = B )
5	3, 4	neeqtrrd 2868	1 |- ( ph -> C =/= D )

Syntax hints:   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  infpssrlem4  9128  modsumfzodifsn  12743  mgm2nsgrplem4  17408  pmtr3ncomlem1  17893  isdrng2  18757  prmirredlem  19841  uvcf1  20131  dfac14lem  21420  i1fmullem  23461  fta1glem1  23925  fta1blem  23928  plydivlem4  24051  fta1lem  24062  cubic  24576  asinlem  24595  dchrn0  24975  lgsne0  25060  perpneq  25609  axlowdimlem14  25835  cntnevol  30291  subfacp1lem5  31166  noextenddif  31821  noresle  31846  fvtransport  32139  poimirlem1  33410  poimirlem6  33415  poimirlem7  33416  dalem4  34951  cdleme35sn2aw  35746  cdleme39n  35754  cdleme41fva11  35765  trlcone  36016  hdmap1neglem1N  37117  hdmaprnlem3N  37142  stoweidlem23  40240  2zrngnmlid  41949  2zrngnmrid  41950  zlmodzxznm  42286