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

Theorem necon3bd 3030
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 3020 . . 3 𝐴𝐵𝐴 = 𝐵)
2 necon3bd.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
31, 2syl5bi 243 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
43con1d 147 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon2ad  3031  nelne1OLD  3114  nelne2OLD  3116  nssne1  4026  nssne2  4027  disjne  4402  nbrne1  5077  nbrne2  5078  peano5  7593  oeeui  8218  domdifsn  8589  ac6sfi  8751  inf3lem2  9081  cnfcom3lem  9155  dfac9  9551  fin23lem21  9750  dedekindle  10793  zneo  12054  modirr  13300  sqrmo  14601  reusq0  14812  pc2dvds  16205  pcadd  16215  oddprmdvds  16229  4sqlem11  16281  latnlej  17668  sylow2blem3  18678  irredn0  19384  irredn1  19387  lssvneln0  19654  lspsnne2  19821  lspfixed  19831  lspindpi  19835  lsmcv  19844  lspsolv  19846  isnzr2  19966  coe1tmmul  20375  dfac14  22156  fbdmn0  22372  filufint  22458  flimfnfcls  22566  alexsubALTlem2  22586  evth  23492  cphsqrtcl2  23719  ovolicc2lem4  24050  lhop1lem  24539  lhop1  24540  lhop2  24541  lhop  24542  deg1add  24626  abelthlem2  24949  logcnlem2  25153  angpined  25335  asinneg  25391  dmgmaddn0  25528  lgsne0  25839  lgsqr  25855  lgsquadlem2  25885  lgsquadlem3  25886  axlowdimlem17  26672  spansncvi  29357  broutsideof2  33481  unblimceq0lem  33743  poimirlem28  34802  dvasin  34860  dvacos  34861  nninfnub  34909  dvrunz  35115  lsatcvatlem  36067  lkrlsp2  36121  opnlen0  36206  2llnne2N  36426  lnnat  36445  llnn0  36534  lplnn0N  36565  lplnllnneN  36574  llncvrlpln2  36575  llncvrlpln  36576  lvoln0N  36609  lplncvrlvol2  36633  lplncvrlvol  36634  dalempnes  36669  dalemqnet  36670  dalemcea  36678  dalem3  36682  cdlema1N  36809  cdlemb  36812  paddasslem5  36842  llnexchb2lem  36886  osumcllem4N  36977  pexmidlem1N  36988  lhp2lt  37019  lhp2atne  37052  lhp2at0ne  37054  4atexlemunv  37084  4atexlemex2  37089  trlne  37203  trlval4  37206  cdlemc4  37212  cdleme11dN  37280  cdleme11h  37284  cdlemednuN  37318  cdleme20j  37336  cdleme20k  37337  cdleme21at  37346  cdleme35f  37472  cdlemg11b  37660  dia2dimlem1  38082  dihmeetlem3N  38323  dihmeetlem15N  38339  dochsnnz  38468  dochexmidlem1  38478  dochexmidlem7  38484  mapdindp3  38740  fltne  39152  pellexlem1  39306  dfac21  39546  pm13.14  40621  uzlidlring  44098  suppdm  44463
  Copyright terms: Public domain W3C validator