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

Theorem neeq12d 2851
 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 2636 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 2834 1 (𝜑 → (𝐴𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ≠ wne 2790 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-ne 2791 This theorem is referenced by:  fnelnfp  6408  suppval  7257  infpssrlem4  9088  injresinjlem  12544  sgrp2nmndlem5  17356  pmtr3ncom  17835  isnzr  19199  ptcmplem2  21797  isinag  25663  axlowdimlem6  25761  axlowdimlem14  25769  pthdadjvtx  26529  uhgrwkspthlem2  26553  usgr2wlkspth  26558  usgr2trlncl  26559  pthdlem1  26565  lfgrn1cycl  26600  2wlkdlem5  26728  2pthdlem1  26729  3wlkdlem5  26923  3pthdlem1  26924  numclwwlk2lem1  27124  numclwlk2lem2f  27125  numclwlk2lem2f1o  27127  numclwwlk5  27134  eulplig  27225  signsvvfval  30477  signsvfn  30481  bnj1534  30684  bnj1542  30688  bnj1280  30849  derangsn  30913  derangenlem  30914  subfacp1lem3  30925  subfacp1lem5  30927  subfacp1lem6  30928  subfacp1  30929  sltval2  31563  sltres  31571  noseponlem  31575  noextenddif  31578  nodenselem3  31599  nodenselem5  31601  nodenselem7  31603  nosepnelem  31618  fvtransport  31834  poimirlem1  33081  poimirlem6  33086  poimirlem7  33087  cdlemkid3N  35740  cdlemkid4  35741  stoweidlem43  39597  nnsgrpnmnd  41136  2zrngnmlid  41267  pgrpgt2nabl  41465  ldepsnlinc  41615
 Copyright terms: Public domain W3C validator