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

Theorem mtod 197
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1 (𝜑 → ¬ 𝜒)
mtod.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtod (𝜑 → ¬ 𝜓)

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2 (𝜑 → (𝜓𝜒))
2 mtod.1 . . 3 (𝜑 → ¬ 𝜒)
32a1d 25 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
41, 3pm2.65d 195 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mtoi  198  mtbid  324  mtbird  325  mtand  815  mtord  879  po2nr  5564  po3nr  5565  ordn2lp  6342  ordnbtwn  6415  fpropnf1  7219  tfi  7794  nnlim  7821  frrlem14  8235  smoord  8316  tz7.48-3  8395  oalimcl  8512  omlimcl  8530  oneo  8533  omopth2  8536  nnneo  8606  sucdom2OLD  9033  mapdom2  9099  sucdom2  9157  php2  9162  php3OLD  9175  onomeneqOLD  9180  1sdom2dom  9198  isfinite2  9252  domunfican  9271  ordtypelem7  9467  unxpwdom2  9531  cantnfp1lem2  9622  oemapvali  9627  cantnflem1  9632  cantnflem2  9633  rankpwi  9766  tskwe  9893  alephordi  10017  alephdom  10024  cardaleph  10032  cflim2  10206  isfin4p1  10258  fin23lem26  10268  fin1a2lem13  10355  axcclem  10400  fpwwe2lem11  10584  fpwwe2lem12  10585  fpwwe2  10586  pwxpndom2  10608  pwxpndom  10609  pwdjundom  10610  gchaleph  10614  r1wunlim  10680  inatsk  10721  tskuni  10726  gruina  10761  prlem934  10976  dedekind  11325  prodge0rd  13029  qextltlem  13128  ixxub  13292  ixxlb  13293  seqf1olem1  13954  facndiv  14195  cnpart  15132  rlimuni  15439  rlimcld2  15467  isercoll  15559  incexclem  15728  isumltss  15740  alzdvds  16209  fzm1ndvds  16211  fzo0dvdseq  16212  bitsfzolem  16321  smuval2  16369  smupvallem  16370  bezoutlem3  16429  rpdvds  16543  nonsq  16641  prmdiv  16664  odzdvds  16674  pcprendvds  16719  pcprendvds2  16720  pcpremul  16722  pcdvdsb  16748  pcadd2  16769  pockthlem  16784  prmreclem5  16799  prmreclem6  16800  1arith  16806  4sqlem11  16834  vdwlem11  16870  vdwlem12  16871  ramubcl  16897  mrissmrcd  17527  pltnlt  18236  acsfiindd  18449  odcl2  19354  gexnnod  19377  pgpssslw  19403  torsubg  19639  lt6abl  19679  ablfacrplem  19851  pgpfac1lem3  19863  ablsimpnosubgd  19890  irredrmul  20145  islbs3  20632  lbsextlem3  20637  lbsextlem4  20638  rng1nfld  20764  f1lindf  21244  mvrf1  21410  perfopn  22552  pnfnei  22587  mnfnei  22588  haust1  22719  cmpcld  22769  ptbasfi  22948  fbncp  23206  isfild  23225  fbasfip  23235  filufint  23287  rnelfmlem  23319  fmfnfm  23325  fclscf  23392  ptcmplem3  23421  opnsubg  23475  bldisj  23767  iccntr  24200  icccmplem2  24202  reconnlem1  24205  reconnlem2  24206  evth  24338  lebnumlem3  24342  ovolicc2lem3  24899  volfiniun  24927  iundisj  24928  dvne0  25391  lhop2  25395  itgsubstlem  25428  coemullem  25627  plyexmo  25689  logccne0  25950  lgamgulmlem1  26394  wilthlem2  26434  wilth  26436  mumul  26546  chtublem  26575  perfect1  26592  lgsdilem2  26697  lgsne0  26699  lgsqrlem2  26711  lgseisenlem1  26739  lgseisenlem2  26740  lgsquadlem1  26744  lgsquadlem2  26745  lgsquadlem3  26746  lgsquad2lem1  26748  2sqblem  26795  chebbnd1lem1  26833  pntpbnd2  26951  pntlem3  26973  ostth  27003  sltval2  27020  nolt02o  27059  nosupbnd1lem2  27073  nosupbnd1  27078  nosupbnd2  27080  noinfbnd1lem2  27088  noinfbnd1  27093  noinfbnd2  27095  noetasuplem4  27100  noetainflem4  27104  scutbdaybnd2lim  27178  umgrnloop0  28102  usgrnloop0ALT  28195  wlkp1lem2  28664  pthdlem2lem  28757  chirredlem1  31374  iundisjf  31549  ofpreima2  31624  iundisjfi  31741  fundmpss  34380  dfon2lem4  34400  dfon2lem7  34403  broutsideof2  34736  outsidele  34746  nn0prpwlem  34823  onint1  34950  fin2so  36094  lindsadd  36100  lpssat  37504  exatleN  37896  3noncolr2  37941  4noncolr3  37945  3dimlem3  37953  3dimlem3OLDN  37954  3dimlem4a  37955  3dimlem4  37956  3dimlem4OLDN  37957  3atlem4  37978  3atlem5  37979  3atlem6  37980  llnnleat  38005  lplnnle2at  38033  lvolnle3at  38074  4atlem0a  38085  4atlem0ae  38086  dalem21  38186  dalem54  38218  cdlemblem  38285  lhpmcvr4N  38518  4atexlemnclw  38562  cdlemd3  38692  cdleme3g  38726  cdleme3h  38727  cdleme7aa  38734  cdleme7d  38738  cdleme7ga  38740  cdleme11c  38753  cdleme15b  38767  cdleme20zN  38793  cdleme21b  38818  cdleme21c  38819  cdleme21ct  38821  cdleme22b  38833  cdleme32b  38934  cdleme35fnpq  38941  cdleme35f  38946  cdleme36a  38952  cdleme42c  38964  cdleme48bw  38994  cdlemf1  39053  cdlemg2fv2  39092  cdlemg7fvbwN  39099  cdlemg4  39109  cdlemg6c  39112  cdlemg27a  39184  cdlemg27b  39188  cdlemk3  39325  dia2dimlem1  39556  dihord6apre  39748  dihord6b  39752  dihord5apre  39754  dihglbcpreN  39792  dihmeetlem6  39801  dochnel2  39884  dochexmidlem7  39958  lspindp5  40262  mapdh8b  40272  hdmapip0  40407  aks6d1c2p2  40578  rtprmirr  40862  flt4lem5elem  41018  flt4lem7  41026  nna4b4nsq  41027  pellexlem6  41186  elpell14qr2  41214  pellfundglb  41237  jm2.19  41346  jm2.26lem3  41354  setindtr  41377  harinf  41387  dgraa0p  41505  gneispace0nelrn3  42488
  Copyright terms: Public domain W3C validator