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

Theorem mtod 187
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 185 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  188  mtbid  312  mtbird  313  mtand  688  mtord  689  po2nr  4962  po3nr  4963  ordn2lp  5646  ordnbtwn  5719  tfi  6923  nnlim  6948  smoord  7327  tz7.48-3  7404  oalimcl  7505  omlimcl  7523  oneo  7526  omopth2  7529  nnneo  7596  mapdom2  7994  php3  8009  onomeneq  8013  sucdom2  8019  isfinite2  8081  domunfican  8096  ordtypelem7  8290  unxpwdom2  8354  cantnfp1lem2  8437  oemapvali  8442  cantnflem1  8447  cantnflem2  8448  rankpwi  8547  tskwe  8637  alephordi  8758  alephdom  8765  cardaleph  8773  cflim2  8946  isfin4-3  8998  fin23lem26  9008  fin1a2lem13  9095  axcclem  9140  fpwwe2lem12  9320  fpwwe2lem13  9321  fpwwe2  9322  pwxpndom2  9344  pwxpndom  9345  pwcdandom  9346  gchaleph  9350  r1wunlim  9416  inatsk  9457  tskuni  9462  gruina  9497  prlem934  9712  dedekind  10052  qextltlem  11869  ixxub  12026  ixxlb  12027  seqf1olem1  12660  facndiv  12895  cnpart  13777  rlimuni  14078  rlimcld2  14106  isercoll  14195  incexclem  14356  isumltss  14368  alzdvds  14829  fzm1ndvds  14831  fzo0dvdseq  14832  bitsfzolem  14943  smuval2  14991  smupvallem  14992  bezoutlem3  15045  rpdvds  15161  nonsq  15254  prmdiv  15277  odzdvds  15287  pcprendvds  15332  pcprendvds2  15333  pcpremul  15335  pcdvdsb  15360  pcadd2  15381  pockthlem  15396  prmreclem5  15411  prmreclem6  15412  1arith  15418  4sqlem11  15446  vdwlem11  15482  vdwlem12  15483  ramubcl  15509  mrissmrcd  16072  pltnlt  16740  acsfiindd  16949  odcl2  17754  gexnnod  17775  pgpssslw  17801  torsubg  18029  lt6abl  18068  ablfacrplem  18236  pgpfac1lem3  18248  irredrmul  18479  islbs3  18925  lbsextlem3  18930  lbsextlem4  18931  rng1nfld  19048  mvrf1  19195  f1lindf  19928  perfopn  20747  pnfnei  20782  mnfnei  20783  haust1  20914  cmpcld  20963  ptbasfi  21142  fbncp  21401  isfild  21420  fbasfip  21430  filufint  21482  rnelfmlem  21514  fmfnfm  21520  fclscf  21587  ptcmplem3  21616  opnsubg  21669  bldisj  21961  iccntr  22380  icccmplem2  22382  reconnlem1  22385  reconnlem2  22386  evth  22514  lebnumlem3  22518  ovolicc2lem3  23039  volfiniun  23067  iundisj  23068  dvne0  23523  lhop2  23527  itgsubstlem  23560  coemullem  23755  plyexmo  23817  logccne0  24074  lgamgulmlem1  24500  wilthlem2  24540  wilth  24542  mumul  24652  chtublem  24681  perfect1  24698  lgsdilem2  24803  lgsne0  24805  lgsqrlem2  24817  lgseisenlem1  24845  lgseisenlem2  24846  lgsquadlem1  24850  lgsquadlem2  24851  lgsquadlem3  24852  lgsquad2lem1  24854  2sqblem  24901  chebbnd1lem1  24903  pntpbnd2  25021  pntlem3  25043  ostth  25073  vdgr1a  26227  chirredlem1  28467  iundisjf  28618  ofpreima2  28683  iundisjfi  28776  fundmpss  30744  dfon2lem4  30769  dfon2lem7  30772  sltval2  30887  sltasym  30905  broutsideof2  31233  outsidele  31243  nn0prpwlem  31321  nn0prpw  31322  onint1  31452  fin2so  32390  poimirlem16  32419  lpssat  33142  exatleN  33532  3noncolr2  33577  4noncolr3  33581  3dimlem3  33589  3dimlem3OLDN  33590  3dimlem4a  33591  3dimlem4  33592  3dimlem4OLDN  33593  3atlem4  33614  3atlem5  33615  3atlem6  33616  llnnleat  33641  lplnnle2at  33669  lvolnle3at  33710  4atlem0a  33721  4atlem0ae  33722  dalem21  33822  dalem54  33854  cdlemblem  33921  lhpmcvr4N  34154  4atexlemnclw  34198  cdlemd3  34329  cdleme3g  34363  cdleme3h  34364  cdleme7aa  34371  cdleme7d  34375  cdleme7ga  34377  cdleme11c  34390  cdleme15b  34404  cdleme20zN  34430  cdleme20yOLD  34432  cdleme21b  34456  cdleme21c  34457  cdleme21ct  34459  cdleme22b  34471  cdleme32b  34572  cdleme35fnpq  34579  cdleme35f  34584  cdleme36a  34590  cdleme42c  34602  cdleme48bw  34632  cdlemf1  34691  cdlemg2fv2  34730  cdlemg7fvbwN  34737  cdlemg4  34747  cdlemg6c  34750  cdlemg27a  34822  cdlemg27b  34826  cdlemk3  34963  dia2dimlem1  35195  dihord6apre  35387  dihord6b  35391  dihord5apre  35393  dihglbcpreN  35431  dihmeetlem6  35440  dochnel2  35523  dochexmidlem7  35597  lspindp5  35901  mapdh8b  35911  hdmapip0  36049  pellexlem6  36240  elpell14qr2  36268  pellfundglb  36291  jm2.19  36402  jm2.26lem3  36410  setindtr  36433  harinf  36443  dgraa0p  36562  gneispace0nelrn3  37284  fpropnf1  40184  umgrnloop0  40356  usgrnloop0ALT  40454  1wlkp1lem2  40905  pthdlem2lem  40995
  Copyright terms: Public domain W3C validator