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  3848  po2nr  5588  po3nr  5589  ordn2lp  6387  ordnbtwn  6463  fpropnf1  7272  tfi  7858  nnlim  7885  frrlem14  8305  smoord  8361  tz7.48-3  8440  oalimcl  8554  omlimcl  8572  oneo  8575  omopth2  8578  nnneo  8650  mapdom2  9146  sucdom2  9197  php2  9202  1sdom2dom  9224  isfinite2  9268  domunfican  9291  ordtypelem7  9496  unxpwdom2  9560  cantnfp1lem2  9658  oemapvali  9663  cantnflem1  9668  cantnflem2  9669  rankpwi  9805  tskwe  9955  alephordi  10077  alephdom  10084  cardaleph  10092  cflim2  10265  isfin4p1  10317  fin23lem26  10327  fin1a2lem13  10414  axcclem  10459  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  pwxpndom2  10668  pwxpndom  10669  pwdjundom  10670  gchaleph  10674  r1wunlim  10740  inatsk  10781  tskuni  10786  gruina  10821  prlem934  11036  dedekind  11391  prodge0rd  13143  qextltlem  13246  ixxub  13411  ixxlb  13412  seqf1olem1  14097  facndiv  14344  cnpart  15317  rlimuni  15627  rlimcld2  15655  isercoll  15745  incexclem  15916  isumltss  15928  alzdvds  16403  fzm1ndvds  16405  fzo0dvdseq  16406  bitsfzolem  16517  smuval2  16565  smupvallem  16566  bezoutlem3  16624  rpdvds  16743  nonsq  16843  prmdiv  16869  odzdvds  16880  pcprendvds  16925  pcprendvds2  16926  pcpremul  16928  pcdvdsb  16954  pcadd2  16975  pockthlem  16990  prmreclem5  17005  prmreclem6  17006  1arith  17012  4sqlem11  17040  vdwlem11  17076  vdwlem12  17077  ramubcl  17103  mrissmrcd  17721  pltnlt  18419  acsfiindd  18634  odcl2  19666  gexnnod  19689  pgpssslw  19715  torsubg  19955  lt6abl  19996  ablfacrplem  20168  pgpfac1lem3  20180  ablsimpnosubgd  20207  irredrmul  20542  islbs3  21316  lbsextlem3  21321  lbsextlem4  21322  f1lindf  22009  mvrf1  22172  psdmul  22366  perfopn  23379  pnfnei  23414  mnfnei  23415  haust1  23546  cmpcld  23596  ptbasfi  23775  fbncp  24033  isfild  24052  fbasfip  24062  filufint  24114  rnelfmlem  24146  fmfnfm  24152  fclscf  24219  ptcmplem3  24248  opnsubg  24302  bldisj  24592  iccntr  25016  icccmplem2  25018  reconnlem1  25021  reconnlem2  25022  evth  25155  lebnumlem3  25159  ovolicc2lem3  25715  volfiniun  25743  iundisj  25744  dvne0  26207  lhop2  26211  itgsubstlem  26244  coemullem  26444  plyexmo  26511  logccne0  26780  rtprmirr  26962  lgamgulmlem1  27230  wilthlem2  27270  wilth  27272  mumul  27382  chtublem  27412  perfect1  27429  lgsdilem2  27534  lgsne0  27536  lgsqrlem2  27548  lgseisenlem1  27576  lgseisenlem2  27577  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  lgsquad2lem1  27585  2sqblem  27632  chebbnd1lem1  27670  pntpbnd2  27788  pntlem3  27810  ostth  27840  ltsval2  27857  nolt02o  27896  nosupbnd1lem2  27910  nosupbnd1  27915  nosupbnd2  27917  noinfbnd1lem2  27925  noinfbnd1  27930  noinfbnd2  27932  noetasuplem4  27937  noetainflem4  27941  cutbdaybnd2lim  28027  oniso  28501  bdayfinbndlem1  28697  z12bdaylem1  28700  umgrnloop0  29496  usgrnloop0ALT  29592  wlkp1lem2  30059  pthdlem2lem  30153  chirredlem1  32779  iundisjf  32971  ofpreima2  33048  iundisjfi  33178  rprmndvdsru  33850  antnest  36201  antnestlaw3lem  36202  fundmpss  36279  dfon2lem4  36296  dfon2lem7  36299  broutsideof2  36634  outsidele  36644  nn0prpwlem  36873  onint1  37000  fin2so  38298  lindsadd  38304  suceldisj  39507  lpssat  39827  exatleN  40218  3noncolr2  40263  4noncolr3  40267  3dimlem3  40275  3dimlem3OLDN  40276  3dimlem4a  40277  3dimlem4  40278  3dimlem4OLDN  40279  3atlem4  40300  3atlem5  40301  3atlem6  40302  llnnleat  40327  lplnnle2at  40355  lvolnle3at  40396  4atlem0a  40407  4atlem0ae  40408  dalem21  40508  dalem54  40540  cdlemblem  40607  lhpmcvr4N  40840  4atexlemnclw  40884  cdlemd3  41014  cdleme3g  41048  cdleme3h  41049  cdleme7aa  41056  cdleme7d  41060  cdleme7ga  41062  cdleme11c  41075  cdleme15b  41089  cdleme20zN  41115  cdleme21b  41140  cdleme21c  41141  cdleme21ct  41143  cdleme22b  41155  cdleme32b  41256  cdleme35fnpq  41263  cdleme35f  41268  cdleme36a  41274  cdleme42c  41286  cdleme48bw  41316  cdlemf1  41375  cdlemg2fv2  41414  cdlemg7fvbwN  41421  cdlemg4  41431  cdlemg6c  41434  cdlemg27a  41506  cdlemg27b  41510  cdlemk3  41647  dia2dimlem1  41878  dihord6apre  42070  dihord6b  42074  dihord5apre  42076  dihglbcpreN  42114  dihmeetlem6  42123  dochnel2  42206  dochexmidlem7  42280  lspindp5  42584  mapdh8b  42594  hdmapip0  42729  aks6d1c2p2  42926  flt4lem5elem  43423  flt4lem7  43431  nna4b4nsq  43432  pellexlem6  43601  elpell14qr2  43629  pellfundglb  43652  jm2.19  43760  jm2.26lem3  43768  setindtr  43791  harinf  43801  dgraa0p  43916  tfsconcatb0  44111  gneispace0nelrn3  44908