Theorem mtod 189

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 25	. 2 |- ( ph -> ( ps -> -. ch ) )
4	1, 3	pm2.65d 187	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  190  mtbid  314  mtbird  315  mtand  691  mtord  692  po2nr  5048  po3nr  5049  ordn2lp  5743  ordnbtwn  5816  fpropnf1  6524  tfi  7053  nnlim  7078  smoord  7462  tz7.48-3  7539  oalimcl  7640  omlimcl  7658  oneo  7661  omopth2  7664  nnneo  7731  mapdom2  8131  php3  8146  onomeneq  8150  sucdom2  8156  isfinite2  8218  domunfican  8233  ordtypelem7  8429  unxpwdom2  8493  cantnfp1lem2  8576  oemapvali  8581  cantnflem1  8586  cantnflem2  8587  rankpwi  8686  tskwe  8776  alephordi  8897  alephdom  8904  cardaleph  8912  cflim2  9085  isfin4-3  9137  fin23lem26  9147  fin1a2lem13  9234  axcclem  9279  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  pwxpndom2  9487  pwxpndom  9488  pwcdandom  9489  gchaleph  9493  r1wunlim  9559  inatsk  9600  tskuni  9605  gruina  9640  prlem934  9855  dedekind  10200  qextltlem  12033  ixxub  12196  ixxlb  12197  seqf1olem1  12840  facndiv  13075  cnpart  13980  rlimuni  14281  rlimcld2  14309  isercoll  14398  incexclem  14568  isumltss  14580  alzdvds  15042  fzm1ndvds  15044  fzo0dvdseq  15045  bitsfzolem  15156  smuval2  15204  smupvallem  15205  bezoutlem3  15258  rpdvds  15374  nonsq  15467  prmdiv  15490  odzdvds  15500  pcprendvds  15545  pcprendvds2  15546  pcpremul  15548  pcdvdsb  15573  pcadd2  15594  pockthlem  15609  prmreclem5  15624  prmreclem6  15625  1arith  15631  4sqlem11  15659  vdwlem11  15695  vdwlem12  15696  ramubcl  15722  mrissmrcd  16300  pltnlt  16968  acsfiindd  17177  odcl2  17982  gexnnod  18003  pgpssslw  18029  torsubg  18257  lt6abl  18296  ablfacrplem  18464  pgpfac1lem3  18476  irredrmul  18707  islbs3  19155  lbsextlem3  19160  lbsextlem4  19161  rng1nfld  19278  mvrf1  19425  f1lindf  20161  perfopn  20989  pnfnei  21024  mnfnei  21025  haust1  21156  cmpcld  21205  ptbasfi  21384  fbncp  21643  isfild  21662  fbasfip  21672  filufint  21724  rnelfmlem  21756  fmfnfm  21762  fclscf  21829  ptcmplem3  21858  opnsubg  21911  bldisj  22203  iccntr  22624  icccmplem2  22626  reconnlem1  22629  reconnlem2  22630  evth  22758  lebnumlem3  22762  ovolicc2lem3  23287  volfiniun  23315  iundisj  23316  dvne0  23774  lhop2  23778  itgsubstlem  23811  coemullem  24006  plyexmo  24068  logccne0  24325  lgamgulmlem1  24755  wilthlem2  24795  wilth  24797  mumul  24907  chtublem  24936  perfect1  24953  lgsdilem2  25058  lgsne0  25060  lgsqrlem2  25072  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  2sqblem  25156  chebbnd1lem1  25158  pntpbnd2  25276  pntlem3  25298  ostth  25328  umgrnloop0  26004  usgrnloop0ALT  26097  wlkp1lem2  26571  pthdlem2lem  26663  chirredlem1  29249  iundisjf  29402  ofpreima2  29466  iundisjfi  29555  fundmpss  31664  dfon2lem4  31691  dfon2lem7  31694  sltval2  31809  nolt02o  31845  nosupbnd1lem2  31855  nosupbnd1  31860  nosupbnd2  31862  noetalem3  31865  broutsideof2  32229  outsidele  32239  nn0prpwlem  32317  nn0prpw  32318  onint1  32448  fin2so  33396  poimirlem16  33425  lpssat  34300  exatleN  34690  3noncolr2  34735  4noncolr3  34739  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  3atlem4  34772  3atlem5  34773  3atlem6  34774  llnnleat  34799  lplnnle2at  34827  lvolnle3at  34868  4atlem0a  34879  4atlem0ae  34880  dalem21  34980  dalem54  35012  cdlemblem  35079  lhpmcvr4N  35312  4atexlemnclw  35356  cdlemd3  35487  cdleme3g  35521  cdleme3h  35522  cdleme7aa  35529  cdleme7d  35533  cdleme7ga  35535  cdleme11c  35548  cdleme15b  35562  cdleme20zN  35588  cdleme20yOLD  35590  cdleme21b  35614  cdleme21c  35615  cdleme21ct  35617  cdleme22b  35629  cdleme32b  35730  cdleme35fnpq  35737  cdleme35f  35742  cdleme36a  35748  cdleme42c  35760  cdleme48bw  35790  cdlemf1  35849  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg4  35905  cdlemg6c  35908  cdlemg27a  35980  cdlemg27b  35984  cdlemk3  36121  dia2dimlem1  36353  dihord6apre  36545  dihord6b  36549  dihord5apre  36551  dihglbcpreN  36589  dihmeetlem6  36598  dochnel2  36681  dochexmidlem7  36755  lspindp5  37059  mapdh8b  37069  hdmapip0  37207  pellexlem6  37398  elpell14qr2  37426  pellfundglb  37449  jm2.19  37560  jm2.26lem3  37568  setindtr  37591  harinf  37601  dgraa0p  37719  gneispace0nelrn3  38440