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

Theorem neeq12d 3002
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 2753 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 2985 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  2nreu  4444  fnelnfp  7197  resf1extb  7956  suppval  8187  infpssrlem4  10346  injresinjlem  13826  sgrp2nmndlem5  18942  pmtr3ncom  19493  isnzr  20514  nzrpropd  20520  ptcmplem2  24061  sltval2  27701  sltres  27707  noseponlem  27709  noextenddif  27713  nosepnelem  27724  nosepeq  27730  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  isinag  28846  axlowdimlem6  28962  axlowdimlem14  28970  pthdadjvtx  29748  uhgrwkspthlem2  29774  usgr2wlkspth  29779  usgr2trlncl  29780  pthdlem1  29786  lfgrn1cycl  29825  2wlkdlem5  29949  2pthdlem1  29950  3wlkdlem5  30182  3pthdlem1  30183  numclwwlkovh0  30391  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  eulplig  30504  opprqusdrng  33521  signsvvfval  34593  signsvfn  34597  bnj1534  34867  bnj1542  34871  bnj1280  35034  derangsn  35175  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  subfacp1  35191  fvtransport  36033  irrdiff  37327  poimirlem1  37628  poimirlem6  37633  poimirlem7  37634  cdlemkid3N  40935  cdlemkid4  40936  aks6d1c2p2  42120  hashscontpow  42123  sticksstones1  42147  sticksstones2  42148  stoweidlem43  46058  ichnreuop  47459  isubgr3stgrlem4  47936  gpg5nbgrvtx13starlem2  48028  nnsgrpnmnd  48094  2zrngnmlid  48171  pgrpgt2nabl  48282  ldepsnlinc  48425
  Copyright terms: Public domain W3C validator