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

Theorem neeq12d 3077
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 2837 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 3060 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  2nreu  4391  fnelnfp  6932  suppval  7823  infpssrlem4  9717  injresinjlem  13147  sgrp2nmndlem5  18034  pmtr3ncom  18534  isnzr  19962  ptcmplem2  22591  isinag  26552  axlowdimlem6  26661  axlowdimlem14  26669  pthdadjvtx  27439  uhgrwkspthlem2  27463  usgr2wlkspth  27468  usgr2trlncl  27469  pthdlem1  27475  lfgrn1cycl  27511  2wlkdlem5  27636  2pthdlem1  27637  3wlkdlem5  27870  3pthdlem1  27871  numclwwlkovh0  28079  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  eulplig  28190  signsvvfval  31748  signsvfn  31752  bnj1534  32025  bnj1542  32029  bnj1280  32190  derangsn  32315  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  subfacp1lem6  32330  subfacp1  32331  sltval2  33061  sltres  33067  noseponlem  33069  noextenddif  33073  nosepnelem  33082  nosepeq  33087  nosupbnd2lem1  33113  noetalem3  33117  fvtransport  33391  poimirlem1  34775  poimirlem6  34780  poimirlem7  34781  cdlemkid3N  37951  cdlemkid4  37952  stoweidlem43  42209  ichnreuop  43481  nnsgrpnmnd  43932  2zrngnmlid  44118  pgrpgt2nabl  44312  ldepsnlinc  44461
  Copyright terms: Public domain W3C validator