Theorem mtod 198

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 196	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  199  mtbid  324  mtbird  325  mtand  816  mtord  880  po2nr  5553  po3nr  5554  ordn2lp  6343  ordnbtwn  6418  fpropnf1  7222  tfi  7804  nnlim  7831  frrlem14  8249  smoord  8305  tz7.48-3  8383  oalimcl  8495  omlimcl  8513  oneo  8516  omopth2  8519  nnneo  8591  mapdom2  9086  sucdom2  9137  php2  9142  1sdom2dom  9164  isfinite2  9208  domunfican  9232  ordtypelem7  9439  unxpwdom2  9503  cantnfp1lem2  9600  oemapvali  9605  cantnflem1  9610  cantnflem2  9611  rankpwi  9747  tskwe  9874  alephordi  9996  alephdom  10003  cardaleph  10011  cflim2  10185  isfin4p1  10237  fin23lem26  10247  fin1a2lem13  10334  axcclem  10379  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  gchaleph  10594  r1wunlim  10660  inatsk  10701  tskuni  10706  gruina  10741  prlem934  10956  dedekind  11309  prodge0rd  13051  qextltlem  13154  ixxub  13319  ixxlb  13320  seqf1olem1  14003  facndiv  14250  cnpart  15202  rlimuni  15512  rlimcld2  15540  isercoll  15630  incexclem  15801  isumltss  15813  alzdvds  16289  fzm1ndvds  16291  fzo0dvdseq  16292  bitsfzolem  16403  smuval2  16451  smupvallem  16452  bezoutlem3  16510  rpdvds  16629  nonsq  16729  prmdiv  16755  odzdvds  16766  pcprendvds  16811  pcprendvds2  16812  pcpremul  16814  pcdvdsb  16840  pcadd2  16861  pockthlem  16876  prmreclem5  16891  prmreclem6  16892  1arith  16898  4sqlem11  16926  vdwlem11  16962  vdwlem12  16963  ramubcl  16989  mrissmrcd  17606  pltnlt  18304  acsfiindd  18519  odcl2  19540  gexnnod  19563  pgpssslw  19589  torsubg  19829  lt6abl  19870  ablfacrplem  20042  pgpfac1lem3  20054  ablsimpnosubgd  20081  irredrmul  20407  islbs3  21153  lbsextlem3  21158  lbsextlem4  21159  f1lindf  21802  mvrf1  21964  psdmul  22132  perfopn  23150  pnfnei  23185  mnfnei  23186  haust1  23317  cmpcld  23367  ptbasfi  23546  fbncp  23804  isfild  23823  fbasfip  23833  filufint  23885  rnelfmlem  23917  fmfnfm  23923  fclscf  23990  ptcmplem3  24019  opnsubg  24073  bldisj  24363  iccntr  24787  icccmplem2  24789  reconnlem1  24792  reconnlem2  24793  evth  24926  lebnumlem3  24930  ovolicc2lem3  25486  volfiniun  25514  iundisj  25515  dvne0  25978  lhop2  25982  itgsubstlem  26015  coemullem  26215  plyexmo  26279  logccne0  26542  rtprmirr  26724  lgamgulmlem1  26992  wilthlem2  27032  wilth  27034  mumul  27144  chtublem  27174  perfect1  27191  lgsdilem2  27296  lgsne0  27298  lgsqrlem2  27310  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem1  27347  2sqblem  27394  chebbnd1lem1  27432  pntpbnd2  27550  pntlem3  27572  ostth  27602  ltsval2  27620  nolt02o  27659  nosupbnd1lem2  27673  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1lem2  27688  noinfbnd1  27693  noinfbnd2  27695  noetasuplem4  27700  noetainflem4  27704  cutbdaybnd2lim  27789  oniso  28263  bdayfinbndlem1  28459  z12bdaylem1  28462  umgrnloop0  29178  usgrnloop0ALT  29274  wlkp1lem2  29741  pthdlem2lem  29835  chirredlem1  32461  iundisjf  32659  ofpreima2  32739  iundisjfi  32869  rprmndvdsru  33589  antnest  35871  antnestlaw3lem  35872  fundmpss  35949  dfon2lem4  35966  dfon2lem7  35969  broutsideof2  36304  outsidele  36314  nn0prpwlem  36504  onint1  36631  fin2so  37928  lindsadd  37934  suceldisj  39139  lpssat  39459  exatleN  39850  3noncolr2  39895  4noncolr3  39899  3dimlem3  39907  3dimlem3OLDN  39908  3dimlem4a  39909  3dimlem4  39910  3dimlem4OLDN  39911  3atlem4  39932  3atlem5  39933  3atlem6  39934  llnnleat  39959  lplnnle2at  39987  lvolnle3at  40028  4atlem0a  40039  4atlem0ae  40040  dalem21  40140  dalem54  40172  cdlemblem  40239  lhpmcvr4N  40472  4atexlemnclw  40516  cdlemd3  40646  cdleme3g  40680  cdleme3h  40681  cdleme7aa  40688  cdleme7d  40692  cdleme7ga  40694  cdleme11c  40707  cdleme15b  40721  cdleme20zN  40747  cdleme21b  40772  cdleme21c  40773  cdleme21ct  40775  cdleme22b  40787  cdleme32b  40888  cdleme35fnpq  40895  cdleme35f  40900  cdleme36a  40906  cdleme42c  40918  cdleme48bw  40948  cdlemf1  41007  cdlemg2fv2  41046  cdlemg7fvbwN  41053  cdlemg4  41063  cdlemg6c  41066  cdlemg27a  41138  cdlemg27b  41142  cdlemk3  41279  dia2dimlem1  41510  dihord6apre  41702  dihord6b  41706  dihord5apre  41708  dihglbcpreN  41746  dihmeetlem6  41755  dochnel2  41838  dochexmidlem7  41912  lspindp5  42216  mapdh8b  42226  hdmapip0  42361  aks6d1c2p2  42558  flt4lem5elem  43084  flt4lem7  43092  nna4b4nsq  43093  pellexlem6  43262  elpell14qr2  43290  pellfundglb  43313  jm2.19  43421  jm2.26lem3  43429  setindtr  43452  harinf  43462  dgraa0p  43577  tfsconcatb0  43772  gneispace0nelrn3  44569