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

Step	Hyp	Ref	Expression
1		mtod.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mtod.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	2	a1d 26	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mtoi  202  mtbid  327  mtbird  328  mtand  828  mtord  893  nrmod  3839  po2nr  5573  po3nr  5574  ordn2lp  6375  ordnbtwn  6451  fpropnf1  7263  tfi  7853  nnlim  7880  frrlem14  8301  smoord  8357  tz7.48-3  8438  oalimcl  8552  omlimcl  8570  oneo  8573  omopth2  8576  nnneo  8648  mapdom2  9151  sucdom2  9202  php2  9207  1sdom2dom  9229  isfinite2  9274  domunfican  9297  ordtypelem7  9502  unxpwdom2  9566  cantnfp1lem2  9664  oemapvali  9669  cantnflem1  9674  cantnflem2  9675  rankpwi  9813  tskwe  10012  alephordi  10134  alephdom  10141  cardaleph  10149  cflim2  10322  isfin4p1  10374  fin23lem26  10384  fin1a2lem13  10471  axcclem  10516  fpwwe2lem11  10707  fpwwe2lem12  10708  fpwwe2  10709  pwxpndom2  10731  pwxpndom  10732  pwdjundom  10733  gchaleph  10737  r1wunlim  10803  inatsk  10844  tskuni  10849  gruina  10884  prlem934  11099  dedekind  11454  prodge0rd  13210  qextltlem  13313  ixxub  13478  ixxlb  13479  seqf1olem1  14164  facndiv  14412  cnpart  15387  rlimuni  15697  rlimcld2  15725  isercoll  15815  incexclem  15985  isumltss  15997  alzdvds  16470  fzm1ndvds  16472  fzo0dvdseq  16473  bitsfzolem  16584  smuval2  16632  smupvallem  16633  bezoutlem3  16694  rpdvds  16815  nonsq  16915  prmdiv  16942  odzdvds  16953  pcprendvds  16998  pcprendvds2  16999  pcpremul  17001  pcdvdsb  17027  pcadd2  17048  pockthlem  17063  prmreclem5  17078  prmreclem6  17079  1arith  17085  4sqlem11  17113  vdwlem11  17149  vdwlem12  17150  ramubcl  17176  mrissmrcd  17794  pltnlt  18492  acsfiindd  18707  odcl2  19759  gexnnod  19782  pgpssslw  19808  torsubg  20048  lt6abl  20089  ablfacrplem  20261  pgpfac1lem3  20273  ablsimpnosubgd  20300  irredrmul  20637  islbs3  21413  lbsextlem3  21418  lbsextlem4  21419  f1lindf  22108  mvrf1  22273  psdmul  22467  perfopn  23483  pnfnei  23518  mnfnei  23519  haust1  23650  cmpcld  23700  ptbasfi  23880  fbncp  24138  isfild  24157  fbasfip  24167  filufint  24219  rnelfmlem  24251  fmfnfm  24257  fclscf  24324  ptcmplem3  24353  opnsubg  24407  bldisj  24697  iccntr  25121  icccmplem2  25123  reconnlem1  25126  reconnlem2  25127  evth  25260  lebnumlem3  25264  ovolicc2lem3  25820  volfiniun  25848  iundisj  25849  dvne0  26311  lhop2  26315  itgsubstlem  26348  coemullem  26549  rnplynfin  26612  plyexmo  26618  logccne0  26888  rtprmirr  27070  lgamgulmlem1  27338  wilthlem2  27378  wilth  27380  mumul  27490  chtublem  27520  perfect1  27537  lgsdilem2  27642  lgsne0  27644  lgsqrlem2  27656  lgseisenlem1  27684  lgseisenlem2  27685  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  lgsquad2lem1  27693  2sqblem  27740  chebbnd1lem1  27778  pntpbnd2  27896  pntlem3  27918  ostth  27948  flt4lem5elem  27963  flt4lem7  27971  nna4b4nsq  27972  ltsval2  27995  nolt02o  28034  nosupbnd1lem2  28048  nosupbnd1  28053  nosupbnd2  28055  noinfbnd1lem2  28063  noinfbnd1  28068  noinfbnd2  28070  noetasuplem4  28075  noetainflem4  28079  cutbdaybnd2lim  28165  oniso  28639  bdayfinbndlem1  28835  z12bdaylem1  28838  umgrnloop0  29669  usgrnloop0ALT  29768  wlkp1lem2  30235  pthdlem2lem  30335  chirredlem1  32974  iundisjf  33165  ofpreima2  33242  iundisjfi  33370  rprmndvdsru  34043  antnest  36423  antnestlaw3lem  36424  fundmpss  36501  dfon2lem4  36518  dfon2lem7  36521  broutsideof2  36857  outsidele  36867  nn0prpwlem  37080  onint1  37207  fin2so  38498  lindsadd  38504  suceldisj  39718  lpssat  40038  exatleN  40429  3noncolr2  40474  4noncolr3  40478  3dimlem3  40486  3dimlem3OLDN  40487  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  3atlem4  40511  3atlem5  40512  3atlem6  40513  llnnleat  40538  lplnnle2at  40566  lvolnle3at  40607  4atlem0a  40618  4atlem0ae  40619  dalem21  40719  dalem54  40751  cdlemblem  40818  lhpmcvr4N  41051  4atexlemnclw  41095  cdlemd3  41225  cdleme3g  41259  cdleme3h  41260  cdleme7aa  41267  cdleme7d  41271  cdleme7ga  41273  cdleme11c  41286  cdleme15b  41300  cdleme20zN  41326  cdleme21b  41351  cdleme21c  41352  cdleme21ct  41354  cdleme22b  41366  cdleme32b  41467  cdleme35fnpq  41474  cdleme35f  41479  cdleme36a  41485  cdleme42c  41497  cdleme48bw  41527  cdlemf1  41586  cdlemg2fv2  41625  cdlemg7fvbwN  41632  cdlemg4  41642  cdlemg6c  41645  cdlemg27a  41717  cdlemg27b  41721  cdlemk3  41858  dia2dimlem1  42089  dihord6apre  42281  dihord6b  42285  dihord5apre  42287  dihglbcpreN  42325  dihmeetlem6  42334  dochnel2  42417  dochexmidlem7  42491  lspindp5  42795  mapdh8b  42805  hdmapip0  42940  aks6d1c2p2  43137  pellexlem6  43794  elpell14qr2  43822  pellfundglb  43845  jm2.19  43953  jm2.26lem3  43961  setindtr  43984  harinf  43994  dgraa0p  44109  tfsconcatb0  44304  gneispace0nelrn3  45101  nellindf  50914