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

Theorem mtod 201
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 199 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  202  mtbid  327  mtbird  328  mtand  815  mtord  877  po2nr  5451  po3nr  5452  ordn2lp  6179  ordnbtwn  6249  fpropnf1  7003  tfi  7548  nnlim  7573  smoord  7985  tz7.48-3  8063  oalimcl  8169  omlimcl  8187  oneo  8190  omopth2  8193  nnneo  8261  sucdom2  8610  mapdom2  8672  php3  8687  onomeneq  8693  isfinite2  8760  domunfican  8775  ordtypelem7  8972  unxpwdom2  9036  cantnfp1lem2  9126  oemapvali  9131  cantnflem1  9136  cantnflem2  9137  rankpwi  9236  tskwe  9363  alephordi  9485  alephdom  9492  cardaleph  9500  cflim2  9674  isfin4p1  9726  fin23lem26  9736  fin1a2lem13  9823  axcclem  9868  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  pwxpndom2  10076  pwxpndom  10077  pwdjundom  10078  gchaleph  10082  r1wunlim  10148  inatsk  10189  tskuni  10194  gruina  10229  prlem934  10444  dedekind  10792  prodge0rd  12484  qextltlem  12583  ixxub  12747  ixxlb  12748  seqf1olem1  13405  facndiv  13644  cnpart  14591  rlimuni  14899  rlimcld2  14927  isercoll  15016  incexclem  15183  isumltss  15195  alzdvds  15662  fzm1ndvds  15664  fzo0dvdseq  15665  bitsfzolem  15773  smuval2  15821  smupvallem  15822  bezoutlem3  15879  rpdvds  15994  nonsq  16089  prmdiv  16112  odzdvds  16122  pcprendvds  16167  pcprendvds2  16168  pcpremul  16170  pcdvdsb  16195  pcadd2  16216  pockthlem  16231  prmreclem5  16246  prmreclem6  16247  1arith  16253  4sqlem11  16281  vdwlem11  16317  vdwlem12  16318  ramubcl  16344  mrissmrcd  16903  pltnlt  17570  acsfiindd  17779  odcl2  18684  gexnnod  18705  pgpssslw  18731  torsubg  18967  lt6abl  19008  ablfacrplem  19180  pgpfac1lem3  19192  ablsimpnosubgd  19219  irredrmul  19453  islbs3  19920  lbsextlem3  19925  lbsextlem4  19926  rng1nfld  20044  f1lindf  20511  mvrf1  20663  perfopn  21790  pnfnei  21825  mnfnei  21826  haust1  21957  cmpcld  22007  ptbasfi  22186  fbncp  22444  isfild  22463  fbasfip  22473  filufint  22525  rnelfmlem  22557  fmfnfm  22563  fclscf  22630  ptcmplem3  22659  opnsubg  22713  bldisj  23005  iccntr  23426  icccmplem2  23428  reconnlem1  23431  reconnlem2  23432  evth  23564  lebnumlem3  23568  ovolicc2lem3  24123  volfiniun  24151  iundisj  24152  dvne0  24614  lhop2  24618  itgsubstlem  24651  coemullem  24847  plyexmo  24909  logccne0  25170  lgamgulmlem1  25614  wilthlem2  25654  wilth  25656  mumul  25766  chtublem  25795  perfect1  25812  lgsdilem2  25917  lgsne0  25919  lgsqrlem2  25931  lgseisenlem1  25959  lgseisenlem2  25960  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  lgsquad2lem1  25968  2sqblem  26015  chebbnd1lem1  26053  pntpbnd2  26171  pntlem3  26193  ostth  26223  umgrnloop0  26902  usgrnloop0ALT  26995  wlkp1lem2  27464  pthdlem2lem  27556  chirredlem1  30173  iundisjf  30352  ofpreima2  30429  iundisjfi  30545  fundmpss  33119  dfon2lem4  33141  dfon2lem7  33144  frrlem14  33246  sltval2  33273  nolt02o  33309  nosupbnd1lem2  33319  nosupbnd1  33324  nosupbnd2  33326  noetalem3  33329  broutsideof2  33693  outsidele  33703  nn0prpwlem  33780  onint1  33907  fin2so  35041  lindsadd  35047  poimirlem16  35070  lpssat  36306  exatleN  36697  3noncolr2  36742  4noncolr3  36746  3dimlem3  36754  3dimlem3OLDN  36755  3dimlem4a  36756  3dimlem4  36757  3dimlem4OLDN  36758  3atlem4  36779  3atlem5  36780  3atlem6  36781  llnnleat  36806  lplnnle2at  36834  lvolnle3at  36875  4atlem0a  36886  4atlem0ae  36887  dalem21  36987  dalem54  37019  cdlemblem  37086  lhpmcvr4N  37319  4atexlemnclw  37363  cdlemd3  37493  cdleme3g  37527  cdleme3h  37528  cdleme7aa  37535  cdleme7d  37539  cdleme7ga  37541  cdleme11c  37554  cdleme15b  37568  cdleme20zN  37594  cdleme21b  37619  cdleme21c  37620  cdleme21ct  37622  cdleme22b  37634  cdleme32b  37735  cdleme35fnpq  37742  cdleme35f  37747  cdleme36a  37753  cdleme42c  37765  cdleme48bw  37795  cdlemf1  37854  cdlemg2fv2  37893  cdlemg7fvbwN  37900  cdlemg4  37910  cdlemg6c  37913  cdlemg27a  37985  cdlemg27b  37989  cdlemk3  38126  dia2dimlem1  38357  dihord6apre  38549  dihord6b  38553  dihord5apre  38555  dihglbcpreN  38593  dihmeetlem6  38602  dochnel2  38685  dochexmidlem7  38759  lspindp5  39063  mapdh8b  39073  hdmapip0  39208  rtprmirr  39497  pellexlem6  39770  elpell14qr2  39798  pellfundglb  39821  jm2.19  39929  jm2.26lem3  39937  setindtr  39960  harinf  39970  dgraa0p  40088  gneispace0nelrn3  40840
  Copyright terms: Public domain W3C validator