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 2749 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 2985 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  2nreu  4402  fnelnfp  7124  suppval  8095  infpssrlem4  10247  injresinjlem  13698  sgrp2nmndlem5  18744  pmtr3ncom  19262  lringring  20194  lringnz  20195  lringuplu  20196  isnzr  20745  ptcmplem2  23420  sltval2  27020  sltres  27026  noseponlem  27028  noextenddif  27032  nosepnelem  27043  nosepeq  27049  nosupbnd2lem1  27079  noinfbnd2lem1  27094  noetasuplem4  27100  noetainflem4  27104  isinag  27822  axlowdimlem6  27938  axlowdimlem14  27946  pthdadjvtx  28720  uhgrwkspthlem2  28744  usgr2wlkspth  28749  usgr2trlncl  28750  pthdlem1  28756  lfgrn1cycl  28792  2wlkdlem5  28916  2pthdlem1  28917  3wlkdlem5  29149  3pthdlem1  29150  numclwwlkovh0  29358  numclwwlk2lem1  29362  numclwlk2lem2f  29363  numclwlk2lem2f1o  29365  eulplig  29469  signsvvfval  33247  signsvfn  33251  bnj1534  33522  bnj1542  33526  bnj1280  33689  derangsn  33821  derangenlem  33822  subfacp1lem3  33833  subfacp1lem5  33835  subfacp1lem6  33836  subfacp1  33837  fvtransport  34663  irrdiff  35843  poimirlem1  36125  poimirlem6  36130  poimirlem7  36131  cdlemkid3N  39442  cdlemkid4  39443  aks6d1c2p2  40595  sticksstones1  40600  sticksstones2  40601  stoweidlem43  44370  ichnreuop  45750  nnsgrpnmnd  46198  2zrngnmlid  46333  pgrpgt2nabl  46528  ldepsnlinc  46675
  Copyright terms: Public domain W3C validator