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 25	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

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  816  mtord  880  po2nr  5467  po3nr  5468  ordn2lp  6211  ordnbtwn  6281  fpropnf1  7057  tfi  7610  nnlim  7636  frrlem14  8018  smoord  8080  tz7.48-3  8158  oalimcl  8266  omlimcl  8284  oneo  8287  omopth2  8290  nnneo  8358  sucdom2  8733  mapdom2  8795  php3  8810  onomeneq  8845  isfinite2  8907  domunfican  8922  ordtypelem7  9118  unxpwdom2  9182  cantnfp1lem2  9272  oemapvali  9277  cantnflem1  9282  cantnflem2  9283  rankpwi  9404  tskwe  9531  alephordi  9653  alephdom  9660  cardaleph  9668  cflim2  9842  isfin4p1  9894  fin23lem26  9904  fin1a2lem13  9991  axcclem  10036  fpwwe2lem11  10220  fpwwe2lem12  10221  fpwwe2  10222  pwxpndom2  10244  pwxpndom  10245  pwdjundom  10246  gchaleph  10250  r1wunlim  10316  inatsk  10357  tskuni  10362  gruina  10397  prlem934  10612  dedekind  10960  prodge0rd  12658  qextltlem  12757  ixxub  12921  ixxlb  12922  seqf1olem1  13580  facndiv  13819  cnpart  14768  rlimuni  15076  rlimcld2  15104  isercoll  15196  incexclem  15363  isumltss  15375  alzdvds  15844  fzm1ndvds  15846  fzo0dvdseq  15847  bitsfzolem  15956  smuval2  16004  smupvallem  16005  bezoutlem3  16064  rpdvds  16180  nonsq  16278  prmdiv  16301  odzdvds  16311  pcprendvds  16356  pcprendvds2  16357  pcpremul  16359  pcdvdsb  16385  pcadd2  16406  pockthlem  16421  prmreclem5  16436  prmreclem6  16437  1arith  16443  4sqlem11  16471  vdwlem11  16507  vdwlem12  16508  ramubcl  16534  mrissmrcd  17097  pltnlt  17800  acsfiindd  18013  odcl2  18910  gexnnod  18931  pgpssslw  18957  torsubg  19193  lt6abl  19234  ablfacrplem  19406  pgpfac1lem3  19418  ablsimpnosubgd  19445  irredrmul  19679  islbs3  20146  lbsextlem3  20151  lbsextlem4  20152  rng1nfld  20270  f1lindf  20738  mvrf1  20904  perfopn  22036  pnfnei  22071  mnfnei  22072  haust1  22203  cmpcld  22253  ptbasfi  22432  fbncp  22690  isfild  22709  fbasfip  22719  filufint  22771  rnelfmlem  22803  fmfnfm  22809  fclscf  22876  ptcmplem3  22905  opnsubg  22959  bldisj  23250  iccntr  23672  icccmplem2  23674  reconnlem1  23677  reconnlem2  23678  evth  23810  lebnumlem3  23814  ovolicc2lem3  24370  volfiniun  24398  iundisj  24399  dvne0  24862  lhop2  24866  itgsubstlem  24899  coemullem  25098  plyexmo  25160  logccne0  25421  lgamgulmlem1  25865  wilthlem2  25905  wilth  25907  mumul  26017  chtublem  26046  perfect1  26063  lgsdilem2  26168  lgsne0  26170  lgsqrlem2  26182  lgseisenlem1  26210  lgseisenlem2  26211  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  lgsquad2lem1  26219  2sqblem  26266  chebbnd1lem1  26304  pntpbnd2  26422  pntlem3  26444  ostth  26474  umgrnloop0  27154  usgrnloop0ALT  27247  wlkp1lem2  27716  pthdlem2lem  27808  chirredlem1  30425  iundisjf  30601  ofpreima2  30677  iundisjfi  30791  fundmpss  33410  dfon2lem4  33432  dfon2lem7  33435  sltval2  33545  nolt02o  33584  nosupbnd1lem2  33598  nosupbnd1  33603  nosupbnd2  33605  noinfbnd1lem2  33613  noinfbnd1  33618  noinfbnd2  33620  noetasuplem4  33625  noetainflem4  33629  scutbdaybnd2lim  33697  broutsideof2  34110  outsidele  34120  nn0prpwlem  34197  onint1  34324  fin2so  35450  lindsadd  35456  lpssat  36713  exatleN  37104  3noncolr2  37149  4noncolr3  37153  3dimlem3  37161  3dimlem3OLDN  37162  3dimlem4a  37163  3dimlem4  37164  3dimlem4OLDN  37165  3atlem4  37186  3atlem5  37187  3atlem6  37188  llnnleat  37213  lplnnle2at  37241  lvolnle3at  37282  4atlem0a  37293  4atlem0ae  37294  dalem21  37394  dalem54  37426  cdlemblem  37493  lhpmcvr4N  37726  4atexlemnclw  37770  cdlemd3  37900  cdleme3g  37934  cdleme3h  37935  cdleme7aa  37942  cdleme7d  37946  cdleme7ga  37948  cdleme11c  37961  cdleme15b  37975  cdleme20zN  38001  cdleme21b  38026  cdleme21c  38027  cdleme21ct  38029  cdleme22b  38041  cdleme32b  38142  cdleme35fnpq  38149  cdleme35f  38154  cdleme36a  38160  cdleme42c  38172  cdleme48bw  38202  cdlemf1  38261  cdlemg2fv2  38300  cdlemg7fvbwN  38307  cdlemg4  38317  cdlemg6c  38320  cdlemg27a  38392  cdlemg27b  38396  cdlemk3  38533  dia2dimlem1  38764  dihord6apre  38956  dihord6b  38960  dihord5apre  38962  dihglbcpreN  39000  dihmeetlem6  39009  dochnel2  39092  dochexmidlem7  39166  lspindp5  39470  mapdh8b  39480  hdmapip0  39615  rtprmirr  39996  flt4lem5elem  40132  flt4lem7  40140  nna4b4nsq  40141  pellexlem6  40300  elpell14qr2  40328  pellfundglb  40351  jm2.19  40459  jm2.26lem3  40467  setindtr  40490  harinf  40500  dgraa0p  40618  gneispace0nelrn3  41370