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

Theorem necon3bd 3028
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3bd.1 (𝜑 → (𝐴 = 𝐵𝜓))
Assertion
Ref Expression
necon3bd (𝜑 → (¬ 𝜓𝐴𝐵))

Proof of Theorem necon3bd
StepHypRef Expression
1 nne 3018 . . 3 𝐴𝐵𝐴 = 𝐵)
2 necon3bd.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
31, 2syl5bi 245 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
43con1d 147 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 3014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-ne 3015
This theorem is referenced by:  necon2ad  3029  nssne1  4013  nssne2  4014  disjne  4387  nbrne1  5071  nbrne2  5072  peano5  7599  oeeui  8224  domdifsn  8596  ac6sfi  8759  inf3lem2  9089  cnfcom3lem  9163  dfac9  9560  fin23lem21  9759  dedekindle  10802  zneo  12062  modirr  13314  sqrmo  14611  reusq0  14822  pc2dvds  16213  pcadd  16223  oddprmdvds  16237  4sqlem11  16289  latnlej  17678  sylow2blem3  18747  irredn0  19456  irredn1  19459  lssvneln0  19723  lspsnne2  19890  lspfixed  19900  lspindpi  19904  lsmcv  19913  lspsolv  19915  isnzr2  20036  coe1tmmul  20445  dfac14  22226  fbdmn0  22442  filufint  22528  flimfnfcls  22636  alexsubALTlem2  22656  evth  23567  cphsqrtcl2  23794  ovolicc2lem4  24127  lhop1lem  24619  lhop1  24620  lhop2  24621  lhop  24622  deg1add  24707  abelthlem2  25030  logcnlem2  25237  angpined  25419  asinneg  25475  dmgmaddn0  25611  lgsne0  25922  lgsqr  25938  lgsquadlem2  25968  lgsquadlem3  25969  axlowdimlem17  26755  spansncvi  29438  broutsideof2  33640  unblimceq0lem  33902  poimirlem28  35030  dvasin  35086  dvacos  35087  nninfnub  35134  dvrunz  35337  lsatcvatlem  36290  lkrlsp2  36344  opnlen0  36429  2llnne2N  36649  lnnat  36668  llnn0  36757  lplnn0N  36788  lplnllnneN  36797  llncvrlpln2  36798  llncvrlpln  36799  lvoln0N  36832  lplncvrlvol2  36856  lplncvrlvol  36857  dalempnes  36892  dalemqnet  36893  dalemcea  36901  dalem3  36905  cdlema1N  37032  cdlemb  37035  paddasslem5  37065  llnexchb2lem  37109  osumcllem4N  37200  pexmidlem1N  37211  lhp2lt  37242  lhp2atne  37275  lhp2at0ne  37277  4atexlemunv  37307  4atexlemex2  37312  trlne  37426  trlval4  37429  cdlemc4  37435  cdleme11dN  37503  cdleme11h  37507  cdlemednuN  37541  cdleme20j  37559  cdleme20k  37560  cdleme21at  37569  cdleme35f  37695  cdlemg11b  37883  dia2dimlem1  38305  dihmeetlem3N  38546  dihmeetlem15N  38562  dochsnnz  38691  dochexmidlem1  38701  dochexmidlem7  38707  mapdindp3  38963  fltne  39532  pellexlem1  39686  dfac21  39926  pm13.14  41033  uzlidlring  44479  suppdm  44845
  Copyright terms: Public domain W3C validator