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

Theorem neeq12d 3075
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 2840 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 3058 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wne 3014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-ne 3015
This theorem is referenced by:  2nreu  4375  fnelnfp  6927  suppval  7822  infpssrlem4  9720  injresinjlem  13157  sgrp2nmndlem5  18090  pmtr3ncom  18599  isnzr  20025  ptcmplem2  22654  isinag  26628  axlowdimlem6  26737  axlowdimlem14  26745  pthdadjvtx  27515  uhgrwkspthlem2  27539  usgr2wlkspth  27544  usgr2trlncl  27545  pthdlem1  27551  lfgrn1cycl  27587  2wlkdlem5  27711  2pthdlem1  27712  3wlkdlem5  27944  3pthdlem1  27945  numclwwlkovh0  28153  numclwwlk2lem1  28157  numclwlk2lem2f  28158  numclwlk2lem2f1o  28160  eulplig  28264  signsvvfval  31873  signsvfn  31877  bnj1534  32150  bnj1542  32154  bnj1280  32317  derangsn  32442  derangenlem  32443  subfacp1lem3  32454  subfacp1lem5  32456  subfacp1lem6  32457  subfacp1  32458  sltval2  33188  sltres  33194  noseponlem  33196  noextenddif  33200  nosepnelem  33209  nosepeq  33214  nosupbnd2lem1  33240  noetalem3  33244  fvtransport  33518  irrdiff  34653  poimirlem1  34968  poimirlem6  34973  poimirlem7  34974  cdlemkid3N  38139  cdlemkid4  38140  stoweidlem43  42548  ichnreuop  43852  nnsgrpnmnd  44301  2zrngnmlid  44436  pgrpgt2nabl  44630  ldepsnlinc  44779
  Copyright terms: Public domain W3C validator