MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3netr4d Structured version   Unicode version

Theorem 3netr4d 2759
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
StepHypRef Expression
1 3netr4d.2 . . 3  |-  ( ph  ->  C  =  A )
2 3netr4d.1 . . 3  |-  ( ph  ->  A  =/=  B )
31, 2eqnetrd 2747 . 2  |-  ( ph  ->  C  =/=  B )
4 3netr4d.3 . 2  |-  ( ph  ->  D  =  B )
53, 4neeqtrrd 2754 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651
This theorem is referenced by:  infpssrlem4  8677  mgm2nsgrplem4  16238  pmtr3ncomlem1  16697  isdrng2  17601  prmirredlem  18705  uvcf1  18994  dfac14lem  20284  i1fmullem  22267  fta1glem1  22732  fta1blem  22735  plydivlem4  22858  fta1lem  22869  cubic  23377  asinlem  23396  dchrn0  23723  lgsne0  23806  perpneq  24292  axlowdimlem14  24460  cntnevol  28436  subfacp1lem5  28892  nofulllem4  29705  fvtransport  29910  stoweidlem23  32044  2zrngnmlid  33009  2zrngnmrid  33010  zlmodzxznm  33352  dalem4  35786  cdleme35sn2aw  36581  cdleme39n  36589  cdleme41fva11  36600  trlcone  36851  hdmap1neglem1N  37952  hdmaprnlem3N  37977
  Copyright terms: Public domain W3C validator