Theorem mtod 177

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 175	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  178  mtbid  300  mtbird  301  mtand  659  mtord  660  po2nr  4813  po3nr  4814  ordn2lp  4898  onssneli  4987  tfi  6672  nnlim  6697  smoord  7036  tz7.48-3  7109  oalimcl  7209  omlimcl  7227  oneo  7230  omopth2  7233  nnneo  7300  mapdom2  7688  php3  7703  onomeneq  7707  sucdom2  7714  isfinite2  7778  domunfican  7793  ordtypelem7  7949  unxpwdom2  8014  cantnfp1lem2  8098  oemapvali  8103  cantnflem1  8108  cantnflem2  8109  cantnfp1lem2OLD  8124  cantnflem1OLD  8131  rankpwi  8241  tskwe  8331  alephordi  8455  alephdom  8462  cardaleph  8470  cflim2  8643  isfin4-3  8695  fin23lem26  8705  fin1a2lem13  8792  axcclem  8837  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  pwxpndom2  9043  pwxpndom  9044  pwcdandom  9045  gchaleph  9049  r1wunlim  9115  inatsk  9156  tskuni  9161  gruina  9196  prlem934  9411  dedekind  9743  qextltlem  11401  ixxub  11550  ixxlb  11551  seqf1olem1  12114  facndiv  12334  cnpart  13036  rlimuni  13336  rlimcld2  13364  isercoll  13453  incexclem  13611  isumltss  13623  alzdvds  13895  fzm1ndvds  13897  fzo0dvdseq  13898  bitsfzolem  13943  smuval2  13991  smupvallem  13992  bezoutlem3  14037  rpdvds  14124  nonsq  14151  prmdiv  14174  odzdvds  14181  pcprendvds  14223  pcprendvds2  14224  pcpremul  14226  pcdvdsb  14251  pcadd2  14268  pockthlem  14282  prmreclem5  14297  prmreclem6  14298  1arith  14304  4sqlem11  14332  vdwlem11  14368  vdwlem12  14369  ramubcl  14395  mrissmrcd  14895  pltnlt  15455  acsfiindd  15664  odcl2  16393  gexnnod  16414  pgpssslw  16440  torsubg  16663  lt6abl  16700  ablfacrplem  16918  pgpfac1lem3  16930  irredrmul  17157  islbs3  17601  lbsextlem3  17606  lbsextlem4  17607  rng1nfld  17725  mvrf1  17880  f1lindf  18652  perfopn  19480  pnfnei  19515  mnfnei  19516  haust1  19647  cmpcld  19696  ptbasfi  19845  fbncp  20103  isfild  20122  fbasfip  20132  filufint  20184  rnelfmlem  20216  fmfnfm  20222  fclscf  20289  ptcmplem3  20317  opnsubg  20369  bldisj  20664  iccntr  21089  icccmplem2  21091  reconnlem1  21094  reconnlem2  21095  evth  21222  lebnumlem3  21226  ovolicc2lem3  21693  volfiniun  21720  iundisj  21721  dvne0  22175  lhop2  22179  itgsubstlem  22212  coemullem  22409  plyexmo  22471  wilthlem2  23099  wilth  23101  mumul  23211  chtublem  23242  perfect1  23259  lgsdilem2  23362  lgsne0  23364  lgsqrlem2  23373  lgseisenlem1  23380  lgseisenlem2  23381  lgsquadlem1  23385  lgsquadlem2  23386  lgsquadlem3  23387  lgsquad2lem1  23389  2sqblem  23408  chebbnd1lem1  23410  pntpbnd2  23528  pntlem3  23550  ostth  23580  vdgr1a  24610  chirredlem1  27013  iundisjf  27149  iundisjfi  27297  logccne0  27680  lgamgulmlem1  28239  fundmpss  28801  dfon2lem4  28823  dfon2lem7  28826  sltval2  29021  sltasym  29037  broutsideof2  29377  outsidele  29387  onint1  29519  fin2so  29645  nn0prpwlem  29745  nn0prpw  29746  pellexlem6  30402  elpell14qr2  30430  pellfundglb  30453  jm2.19  30567  jm2.26lem3  30575  setindtr  30598  harinf  30608  dgraa0p  30731  lpssat  33828  exatleN  34218  3noncolr2  34263  4noncolr3  34267  3dimlem3  34275  3dimlem3OLDN  34276  3dimlem4a  34277  3dimlem4  34278  3dimlem4OLDN  34279  3atlem4  34300  3atlem5  34301  3atlem6  34302  llnnleat  34327  lplnnle2at  34355  lvolnle3at  34396  4atlem0a  34407  4atlem0ae  34408  dalem21  34508  dalem54  34540  cdlemblem  34607  lhpmcvr4N  34840  4atexlemnclw  34884  cdlemd3  35014  cdleme3g  35048  cdleme3h  35049  cdleme7aa  35056  cdleme7d  35060  cdleme7ga  35062  cdleme11c  35075  cdleme15b  35089  cdleme20zN  35115  cdleme20y  35116  cdleme21b  35140  cdleme21c  35141  cdleme21ct  35143  cdleme22b  35155  cdleme32b  35256  cdleme35fnpq  35263  cdleme35f  35268  cdleme36a  35274  cdleme42c  35286  cdleme48bw  35316  cdlemf1  35375  cdlemg2fv2  35414  cdlemg7fvbwN  35421  cdlemg4  35431  cdlemg6c  35434  cdlemg27a  35506  cdlemg27b  35510  cdlemk3  35647  dia2dimlem1  35879  dihord6apre  36071  dihord6b  36075  dihord5apre  36077  dihglbcpreN  36115  dihmeetlem6  36124  dochnel2  36207  dochexmidlem7  36281  lspindp5  36585  mapdh8b  36595  hdmapip0  36733