Theorem mtod 181

Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mtod.1	|- ( ph -> -. ch )
mtod.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mtod	|- ( ph -> -. ps )

Proof of Theorem mtod

Step	Hyp	Ref	Expression
1		mtod.2	. 2 |- ( ph -> ( ps -> ch ) )
2		mtod.1	. . 3 |- ( ph -> -. ch )
3	2	a1d 26	. 2 |- ( ph -> ( ps -> -. ch ) )
4	1, 3	pm2.65d 179	1 |- ( ph -> -. ps )

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  182  mtbid  302  mtbird  303  mtand  665  mtord  666  po2nr  4768  po3nr  4769  ordn2lp  5443  onssneli  5532  tfi  6680  nnlim  6705  smoord  7084  tz7.48-3  7161  oalimcl  7261  omlimcl  7279  oneo  7282  omopth2  7285  nnneo  7352  mapdom2  7743  php3  7758  onomeneq  7762  sucdom2  7768  isfinite2  7829  domunfican  7844  ordtypelem7  8039  unxpwdom2  8103  cantnfp1lem2  8184  oemapvali  8189  cantnflem1  8194  cantnflem2  8195  rankpwi  8294  tskwe  8384  alephordi  8505  alephdom  8512  cardaleph  8520  cflim2  8693  isfin4-3  8745  fin23lem26  8755  fin1a2lem13  8842  axcclem  8887  fpwwe2lem12  9066  fpwwe2lem13  9067  fpwwe2  9068  pwxpndom2  9090  pwxpndom  9091  pwcdandom  9092  gchaleph  9096  r1wunlim  9162  inatsk  9203  tskuni  9208  gruina  9243  prlem934  9458  dedekind  9797  qextltlem  11495  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  seqf1olem1  12252  facndiv  12473  cnpart  13303  rlimuni  13614  rlimcld2  13642  isercoll  13731  incexclem  13894  isumltss  13906  alzdvds  14355  fzm1ndvds  14357  fzo0dvdseq  14358  bitsfzolem  14407  bitsfzolemOLD  14408  smuval2  14456  smupvallem  14457  bezoutlem3OLD  14505  bezoutlem3  14508  rpdvds  14676  nonsq  14708  prmdiv  14733  odzdvds  14740  odzdvdsOLD  14746  pcprendvds  14790  pcprendvds2  14791  pcpremul  14793  pcdvdsb  14818  pcadd2  14835  pockthlem  14849  prmreclem5  14864  prmreclem6  14865  1arith  14871  4sqlem11  14899  vdwlem11  14941  vdwlem12  14942  ramubcl  14976  mrissmrcd  15546  pltnlt  16214  acsfiindd  16423  odcl2  17216  gexnnod  17240  pgpssslw  17266  torsubg  17492  lt6abl  17529  ablfacrplem  17698  pgpfac1lem3  17710  irredrmul  17935  islbs3  18378  lbsextlem3  18383  lbsextlem4  18384  rng1nfld  18502  mvrf1  18649  f1lindf  19380  perfopn  20201  pnfnei  20236  mnfnei  20237  haust1  20368  cmpcld  20417  ptbasfi  20596  fbncp  20854  isfild  20873  fbasfip  20883  filufint  20935  rnelfmlem  20967  fmfnfm  20973  fclscf  21040  ptcmplem3  21069  opnsubg  21122  bldisj  21413  iccntr  21839  icccmplem2  21841  reconnlem1  21844  reconnlem2  21845  evth  21987  lebnumlem3  21991  lebnumlem3OLD  21994  ovolicc2lem3  22472  volfiniun  22500  iundisj  22501  dvne0  22963  lhop2  22967  itgsubstlem  23000  coemullem  23204  plyexmo  23266  logccne0  23528  lgamgulmlem1  23954  wilthlem2  23994  wilth  23996  mumul  24108  chtublem  24139  perfect1  24156  lgsdilem2  24259  lgsne0  24261  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem2  24278  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  lgsquad2lem1  24286  2sqblem  24305  chebbnd1lem1  24307  pntpbnd2  24425  pntlem3  24447  ostth  24477  vdgr1a  25634  chirredlem1  28043  iundisjf  28199  ofpreima2  28269  iundisjfi  28372  fundmpss  30407  dfon2lem4  30432  dfon2lem7  30435  sltval2  30543  sltasym  30561  broutsideof2  30889  outsidele  30899  nn0prpwlem  30978  nn0prpw  30979  onint1  31109  fin2so  31932  poimirlem16  31956  lpssat  32579  exatleN  32969  3noncolr2  33014  4noncolr3  33018  3dimlem3  33026  3dimlem3OLDN  33027  3dimlem4a  33028  3dimlem4  33029  3dimlem4OLDN  33030  3atlem4  33051  3atlem5  33052  3atlem6  33053  llnnleat  33078  lplnnle2at  33106  lvolnle3at  33147  4atlem0a  33158  4atlem0ae  33159  dalem21  33259  dalem54  33291  cdlemblem  33358  lhpmcvr4N  33591  4atexlemnclw  33635  cdlemd3  33766  cdleme3g  33800  cdleme3h  33801  cdleme7aa  33808  cdleme7d  33812  cdleme7ga  33814  cdleme11c  33827  cdleme15b  33841  cdleme20zN  33867  cdleme20yOLD  33869  cdleme21b  33893  cdleme21c  33894  cdleme21ct  33896  cdleme22b  33908  cdleme32b  34009  cdleme35fnpq  34016  cdleme35f  34021  cdleme36a  34027  cdleme42c  34039  cdleme48bw  34069  cdlemf1  34128  cdlemg2fv2  34167  cdlemg7fvbwN  34174  cdlemg4  34184  cdlemg6c  34187  cdlemg27a  34259  cdlemg27b  34263  cdlemk3  34400  dia2dimlem1  34632  dihord6apre  34824  dihord6b  34828  dihord5apre  34830  dihglbcpreN  34868  dihmeetlem6  34877  dochnel2  34960  dochexmidlem7  35034  lspindp5  35338  mapdh8b  35348  hdmapip0  35486  pellexlem6  35678  elpell14qr2  35708  pellfundglb  35733  jm2.19  35848  jm2.26lem3  35856  setindtr  35879  harinf  35889  dgraa0p  36015  fpropnf1  39036  umgrnloop0  39197  usgrnloop0ALT  39288