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

Theorem neeq12d 2884
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 2666 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 2867 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  fnelnfp  6484  suppval  7342  infpssrlem4  9166  injresinjlem  12628  sgrp2nmndlem5  17463  pmtr3ncom  17941  isnzr  19307  ptcmplem2  21904  isinag  25774  axlowdimlem6  25872  axlowdimlem14  25880  pthdadjvtx  26682  uhgrwkspthlem2  26706  usgr2wlkspth  26711  usgr2trlncl  26712  pthdlem1  26718  lfgrn1cycl  26753  2wlkdlem5  26894  2pthdlem1  26895  3wlkdlem5  27141  3pthdlem1  27142  numclwwlkovh0  27352  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  eulplig  27467  signsvvfval  30783  signsvfn  30787  bnj1534  31049  bnj1542  31053  bnj1280  31214  derangsn  31278  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  subfacp1  31294  sltval2  31934  sltres  31940  noseponlem  31942  noextenddif  31946  nosepnelem  31955  nosepeq  31960  nosupbnd2lem1  31986  noetalem3  31990  fvtransport  32264  poimirlem1  33540  poimirlem6  33545  poimirlem7  33546  cdlemkid3N  36538  cdlemkid4  36539  stoweidlem43  40578  nnsgrpnmnd  42143  2zrngnmlid  42274  pgrpgt2nabl  42472  ldepsnlinc  42622
  Copyright terms: Public domain W3C validator