MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq12d Structured version   Visualization version   GIF version

Theorem neeq12d 3029
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
neeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
neeq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem neeq12d
StepHypRef Expression
1 neeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
2 neeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
31, 2eqeq12d 2792 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 3012 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  wne 2968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-ne 2969
This theorem is referenced by:  fnelnfp  6710  suppval  7578  infpssrlem4  9463  injresinjlem  12907  sgrp2nmndlem5  17803  pmtr3ncom  18278  isnzr  19656  ptcmplem2  22265  isinag  26187  axlowdimlem6  26296  axlowdimlem14  26304  pthdadjvtx  27082  uhgrwkspthlem2  27106  usgr2wlkspth  27111  usgr2trlncl  27112  pthdlem1  27118  lfgrn1cycl  27154  2wlkdlem5  27309  2pthdlem1  27310  3wlkdlem5  27580  3pthdlem1  27581  numclwwlkovh0  27814  numclwwlk2lem1  27818  numclwlk2lem2f  27819  numclwlk2lem2f1o  27821  numclwlk2lem2fOLD  27822  numclwlk2lem2f1oOLD  27824  eulplig  27926  signsvvfval  31271  signsvfn  31275  bnj1534  31536  bnj1542  31540  bnj1280  31701  derangsn  31765  derangenlem  31766  subfacp1lem3  31777  subfacp1lem5  31779  subfacp1lem6  31780  subfacp1  31781  sltval2  32412  sltres  32418  noseponlem  32420  noextenddif  32424  nosepnelem  32433  nosepeq  32438  nosupbnd2lem1  32464  noetalem3  32468  fvtransport  32742  poimirlem1  34030  poimirlem6  34035  poimirlem7  34036  cdlemkid3N  37081  cdlemkid4  37082  stoweidlem43  41179  nnsgrpnmnd  42825  2zrngnmlid  42956  pgrpgt2nabl  43154  ldepsnlinc  43304
  Copyright terms: Public domain W3C validator