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

Theorem necon3bd 2796
 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 2786 . . 3 𝐴𝐵𝐴 = 𝐵)
2 necon3bd.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
31, 2syl5bi 231 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
43con1d 138 1 (𝜑 → (¬ 𝜓𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon2ad  2797  nelne1  2878  nelne2  2879  nssne1  3624  nssne2  3625  disjne  3974  nbrne1  4602  nbrne2  4603  peano5  6981  oeeui  7569  domdifsn  7928  ac6sfi  8089  inf3lem2  8409  cnfcom3lem  8483  dfac9  8841  fin23lem21  9044  dedekindle  10080  zneo  11336  modirr  12603  sqrmo  13840  pc2dvds  15421  pcadd  15431  oddprmdvds  15445  4sqlem11  15497  latnlej  16891  sylow2blem3  17860  irredn0  18526  irredn1  18529  lssneln0  18773  lspsnne2  18939  lspfixed  18949  lspindpi  18953  lsmcv  18962  lspsolv  18964  isnzr2  19084  coe1tmmul  19468  dfac14  21231  fbdmn0  21448  filufint  21534  flimfnfcls  21642  alexsubALTlem2  21662  evth  22566  cphsqrtcl2  22794  ovolicc2lem4  23095  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  deg1add  23667  abelthlem2  23990  logcnlem2  24189  angpined  24357  asinneg  24413  dmgmaddn0  24549  lgsne0  24860  lgsqr  24876  lgsquadlem2  24906  lgsquadlem3  24907  axlowdimlem17  25638  spansncvi  27895  broutsideof2  31399  unblimceq0lem  31667  poimirlem28  32607  dvasin  32666  dvacos  32667  nninfnub  32717  dvrunz  32923  lsatcvatlem  33354  lkrlsp2  33408  opnlen0  33493  2llnne2N  33712  lnnat  33731  llnn0  33820  lplnn0N  33851  lplnllnneN  33860  llncvrlpln2  33861  llncvrlpln  33862  lvoln0N  33895  lplncvrlvol2  33919  lplncvrlvol  33920  dalempnes  33955  dalemqnet  33956  dalemcea  33964  dalem3  33968  cdlema1N  34095  cdlemb  34098  paddasslem5  34128  llnexchb2lem  34172  osumcllem4N  34263  pexmidlem1N  34274  lhp2lt  34305  lhp2atne  34338  lhp2at0ne  34340  4atexlemunv  34370  4atexlemex2  34375  trlne  34490  trlval4  34493  cdlemc4  34499  cdleme11dN  34567  cdleme11h  34571  cdlemednuN  34605  cdleme20j  34624  cdleme20k  34625  cdleme21at  34634  cdleme35f  34760  cdlemg11b  34948  dia2dimlem1  35371  dihmeetlem3N  35612  dihmeetlem15N  35628  dochsnnz  35757  dochexmidlem1  35767  dochexmidlem7  35773  mapdindp3  36029  pellexlem1  36411  dfac21  36654  pm13.14  37632  uzlidlring  41719  suppdm  42094
 Copyright terms: Public domain W3C validator