Theorem mtod 197

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 195	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  198  mtbid  324  mtbird  325  mtand  815  mtord  879  po2nr  5601  po3nr  5602  ordn2lp  6381  ordnbtwn  6454  fpropnf1  7261  tfi  7837  nnlim  7864  frrlem14  8279  smoord  8360  tz7.48-3  8439  oalimcl  8556  omlimcl  8574  oneo  8577  omopth2  8580  nnneo  8650  sucdom2OLD  9078  mapdom2  9144  sucdom2  9202  php2  9207  php3OLD  9220  onomeneqOLD  9225  1sdom2dom  9243  isfinite2  9297  domunfican  9316  ordtypelem7  9515  unxpwdom2  9579  cantnfp1lem2  9670  oemapvali  9675  cantnflem1  9680  cantnflem2  9681  rankpwi  9814  tskwe  9941  alephordi  10065  alephdom  10072  cardaleph  10080  cflim2  10254  isfin4p1  10306  fin23lem26  10316  fin1a2lem13  10403  axcclem  10448  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  pwxpndom2  10656  pwxpndom  10657  pwdjundom  10658  gchaleph  10662  r1wunlim  10728  inatsk  10769  tskuni  10774  gruina  10809  prlem934  11024  dedekind  11373  prodge0rd  13077  qextltlem  13177  ixxub  13341  ixxlb  13342  seqf1olem1  14003  facndiv  14244  cnpart  15183  rlimuni  15490  rlimcld2  15518  isercoll  15610  incexclem  15778  isumltss  15790  alzdvds  16259  fzm1ndvds  16261  fzo0dvdseq  16262  bitsfzolem  16371  smuval2  16419  smupvallem  16420  bezoutlem3  16479  rpdvds  16593  nonsq  16691  prmdiv  16714  odzdvds  16724  pcprendvds  16769  pcprendvds2  16770  pcpremul  16772  pcdvdsb  16798  pcadd2  16819  pockthlem  16834  prmreclem5  16849  prmreclem6  16850  1arith  16856  4sqlem11  16884  vdwlem11  16920  vdwlem12  16921  ramubcl  16947  mrissmrcd  17580  pltnlt  18289  acsfiindd  18502  odcl2  19426  gexnnod  19449  pgpssslw  19475  torsubg  19714  lt6abl  19755  ablfacrplem  19927  pgpfac1lem3  19939  ablsimpnosubgd  19966  irredrmul  20230  islbs3  20756  lbsextlem3  20761  lbsextlem4  20762  f1lindf  21361  mvrf1  21527  perfopn  22671  pnfnei  22706  mnfnei  22707  haust1  22838  cmpcld  22888  ptbasfi  23067  fbncp  23325  isfild  23344  fbasfip  23354  filufint  23406  rnelfmlem  23438  fmfnfm  23444  fclscf  23511  ptcmplem3  23540  opnsubg  23594  bldisj  23886  iccntr  24319  icccmplem2  24321  reconnlem1  24324  reconnlem2  24325  evth  24457  lebnumlem3  24461  ovolicc2lem3  25018  volfiniun  25046  iundisj  25047  dvne0  25510  lhop2  25514  itgsubstlem  25547  coemullem  25746  plyexmo  25808  logccne0  26069  lgamgulmlem1  26513  wilthlem2  26553  wilth  26555  mumul  26665  chtublem  26694  perfect1  26711  lgsdilem2  26816  lgsne0  26818  lgsqrlem2  26830  lgseisenlem1  26858  lgseisenlem2  26859  lgsquadlem1  26863  lgsquadlem2  26864  lgsquadlem3  26865  lgsquad2lem1  26867  2sqblem  26914  chebbnd1lem1  26952  pntpbnd2  27070  pntlem3  27092  ostth  27122  sltval2  27139  nolt02o  27178  nosupbnd1lem2  27192  nosupbnd1  27197  nosupbnd2  27199  noinfbnd1lem2  27207  noinfbnd1  27212  noinfbnd2  27214  noetasuplem4  27219  noetainflem4  27223  scutbdaybnd2lim  27298  umgrnloop0  28349  usgrnloop0ALT  28442  wlkp1lem2  28911  pthdlem2lem  29004  chirredlem1  31621  iundisjf  31798  ofpreima2  31869  iundisjfi  31985  fundmpss  34676  dfon2lem4  34696  dfon2lem7  34699  broutsideof2  35032  outsidele  35042  nn0prpwlem  35145  onint1  35272  fin2so  36413  lindsadd  36419  lpssat  37821  exatleN  38213  3noncolr2  38258  4noncolr3  38262  3dimlem3  38270  3dimlem3OLDN  38271  3dimlem4a  38272  3dimlem4  38273  3dimlem4OLDN  38274  3atlem4  38295  3atlem5  38296  3atlem6  38297  llnnleat  38322  lplnnle2at  38350  lvolnle3at  38391  4atlem0a  38402  4atlem0ae  38403  dalem21  38503  dalem54  38535  cdlemblem  38602  lhpmcvr4N  38835  4atexlemnclw  38879  cdlemd3  39009  cdleme3g  39043  cdleme3h  39044  cdleme7aa  39051  cdleme7d  39055  cdleme7ga  39057  cdleme11c  39070  cdleme15b  39084  cdleme20zN  39110  cdleme21b  39135  cdleme21c  39136  cdleme21ct  39138  cdleme22b  39150  cdleme32b  39251  cdleme35fnpq  39258  cdleme35f  39263  cdleme36a  39269  cdleme42c  39281  cdleme48bw  39311  cdlemf1  39370  cdlemg2fv2  39409  cdlemg7fvbwN  39416  cdlemg4  39426  cdlemg6c  39429  cdlemg27a  39501  cdlemg27b  39505  cdlemk3  39642  dia2dimlem1  39873  dihord6apre  40065  dihord6b  40069  dihord5apre  40071  dihglbcpreN  40109  dihmeetlem6  40118  dochnel2  40201  dochexmidlem7  40275  lspindp5  40579  mapdh8b  40589  hdmapip0  40724  aks6d1c2p2  40895  rtprmirr  41181  flt4lem5elem  41337  flt4lem7  41345  nna4b4nsq  41346  pellexlem6  41505  elpell14qr2  41533  pellfundglb  41556  jm2.19  41665  jm2.26lem3  41673  setindtr  41696  harinf  41706  dgraa0p  41824  tfsconcatb0  42027  gneispace0nelrn3  42826