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

Theorem necon3bd 2804
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 2794 . . 3 𝐴𝐵𝐴 = 𝐵)
2 necon3bd.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
31, 2syl5bi 232 . 2 (𝜑 → (¬ 𝐴𝐵𝜓))
43con1d 139 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wne 2790
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 197  df-ne 2791
This theorem is referenced by:  necon2ad  2805  nelne1  2886  nelne2  2887  nssne1  3645  nssne2  3646  disjne  3999  nbrne1  4637  nbrne2  4638  peano5  7043  oeeui  7634  domdifsn  7994  ac6sfi  8155  inf3lem2  8477  cnfcom3lem  8551  dfac9  8909  fin23lem21  9112  dedekindle  10152  zneo  11411  modirr  12688  sqrmo  13933  pc2dvds  15514  pcadd  15524  oddprmdvds  15538  4sqlem11  15590  latnlej  16996  sylow2blem3  17965  irredn0  18631  irredn1  18634  lssneln0  18880  lspsnne2  19046  lspfixed  19056  lspindpi  19060  lsmcv  19069  lspsolv  19071  isnzr2  19191  coe1tmmul  19575  dfac14  21340  fbdmn0  21557  filufint  21643  flimfnfcls  21751  alexsubALTlem2  21771  evth  22677  cphsqrtcl2  22905  ovolicc2lem4  23207  lhop1lem  23693  lhop1  23694  lhop2  23695  lhop  23696  deg1add  23780  abelthlem2  24103  logcnlem2  24302  angpined  24470  asinneg  24526  dmgmaddn0  24662  lgsne0  24973  lgsqr  24989  lgsquadlem2  25019  lgsquadlem3  25020  axlowdimlem17  25751  spansncvi  28378  broutsideof2  31898  unblimceq0lem  32166  poimirlem28  33096  dvasin  33155  dvacos  33156  nninfnub  33206  dvrunz  33412  lsatcvatlem  33843  lkrlsp2  33897  opnlen0  33982  2llnne2N  34201  lnnat  34220  llnn0  34309  lplnn0N  34340  lplnllnneN  34349  llncvrlpln2  34350  llncvrlpln  34351  lvoln0N  34384  lplncvrlvol2  34408  lplncvrlvol  34409  dalempnes  34444  dalemqnet  34445  dalemcea  34453  dalem3  34457  cdlema1N  34584  cdlemb  34587  paddasslem5  34617  llnexchb2lem  34661  osumcllem4N  34752  pexmidlem1N  34763  lhp2lt  34794  lhp2atne  34827  lhp2at0ne  34829  4atexlemunv  34859  4atexlemex2  34864  trlne  34979  trlval4  34982  cdlemc4  34988  cdleme11dN  35056  cdleme11h  35060  cdlemednuN  35094  cdleme20j  35113  cdleme20k  35114  cdleme21at  35123  cdleme35f  35249  cdlemg11b  35437  dia2dimlem1  35860  dihmeetlem3N  36101  dihmeetlem15N  36117  dochsnnz  36246  dochexmidlem1  36256  dochexmidlem7  36262  mapdindp3  36518  pellexlem1  36900  dfac21  37143  pm13.14  38119  uzlidlring  41238  suppdm  41609
  Copyright terms: Public domain W3C validator