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  298  mtbird  299  mtand  657  mtord  658  po2nr  4802  po3nr  4803  ordn2lp  4887  onssneli  4976  tfi  6661  nnlim  6686  smoord  7028  tz7.48-3  7101  oalimcl  7201  omlimcl  7219  oneo  7222  omopth2  7225  nnneo  7292  mapdom2  7681  php3  7696  onomeneq  7700  sucdom2  7707  isfinite2  7770  domunfican  7785  ordtypelem7  7941  unxpwdom2  8006  cantnfp1lem2  8089  oemapvali  8094  cantnflem1  8099  cantnflem2  8100  cantnfp1lem2OLD  8115  cantnflem1OLD  8122  rankpwi  8232  tskwe  8322  alephordi  8446  alephdom  8453  cardaleph  8461  cflim2  8634  isfin4-3  8686  fin23lem26  8696  fin1a2lem13  8783  axcclem  8828  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwe2  9010  pwxpndom2  9032  pwxpndom  9033  pwcdandom  9034  gchaleph  9038  r1wunlim  9104  inatsk  9145  tskuni  9150  gruina  9185  prlem934  9400  dedekind  9733  qextltlem  11404  ixxub  11553  ixxlb  11554  seqf1olem1  12131  facndiv  12351  cnpart  13158  rlimuni  13458  rlimcld2  13486  isercoll  13575  incexclem  13733  isumltss  13745  alzdvds  14123  fzm1ndvds  14125  fzo0dvdseq  14126  bitsfzolem  14171  smuval2  14219  smupvallem  14220  bezoutlem3  14265  rpdvds  14352  nonsq  14379  prmdiv  14402  odzdvds  14409  pcprendvds  14451  pcprendvds2  14452  pcpremul  14454  pcdvdsb  14479  pcadd2  14496  pockthlem  14510  prmreclem5  14525  prmreclem6  14526  1arith  14532  4sqlem11  14560  vdwlem11  14596  vdwlem12  14597  ramubcl  14623  mrissmrcd  15132  pltnlt  15800  acsfiindd  16009  odcl2  16789  gexnnod  16810  pgpssslw  16836  torsubg  17062  lt6abl  17099  ablfacrplem  17314  pgpfac1lem3  17326  irredrmul  17554  islbs3  17999  lbsextlem3  18004  lbsextlem4  18005  rng1nfld  18124  mvrf1  18279  f1lindf  19027  perfopn  19856  pnfnei  19891  mnfnei  19892  haust1  20023  cmpcld  20072  ptbasfi  20251  fbncp  20509  isfild  20528  fbasfip  20538  filufint  20590  rnelfmlem  20622  fmfnfm  20628  fclscf  20695  ptcmplem3  20723  opnsubg  20775  bldisj  21070  iccntr  21495  icccmplem2  21497  reconnlem1  21500  reconnlem2  21501  evth  21628  lebnumlem3  21632  ovolicc2lem3  22099  volfiniun  22126  iundisj  22127  dvne0  22581  lhop2  22585  itgsubstlem  22618  coemullem  22816  plyexmo  22878  logccne0  23135  wilthlem2  23544  wilth  23546  mumul  23656  chtublem  23687  perfect1  23704  lgsdilem2  23807  lgsne0  23809  lgsqrlem2  23818  lgseisenlem1  23825  lgseisenlem2  23826  lgsquadlem1  23830  lgsquadlem2  23831  lgsquadlem3  23832  lgsquad2lem1  23834  2sqblem  23853  chebbnd1lem1  23855  pntpbnd2  23973  pntlem3  23995  ostth  24025  vdgr1a  25111  chirredlem1  27510  iundisjf  27662  ofpreima2  27738  iundisjfi  27838  lgamgulmlem1  28838  fundmpss  29440  dfon2lem4  29461  dfon2lem7  29464  sltval2  29659  sltasym  29675  broutsideof2  30003  outsidele  30013  onint1  30145  fin2so  30283  nn0prpwlem  30383  nn0prpw  30384  pellexlem6  31012  elpell14qr2  31040  pellfundglb  31063  jm2.19  31177  jm2.26lem3  31185  setindtr  31208  harinf  31218  dgraa0p  31342  lpssat  35154  exatleN  35544  3noncolr2  35589  4noncolr3  35593  3dimlem3  35601  3dimlem3OLDN  35602  3dimlem4a  35603  3dimlem4  35604  3dimlem4OLDN  35605  3atlem4  35626  3atlem5  35627  3atlem6  35628  llnnleat  35653  lplnnle2at  35681  lvolnle3at  35722  4atlem0a  35733  4atlem0ae  35734  dalem21  35834  dalem54  35866  cdlemblem  35933  lhpmcvr4N  36166  4atexlemnclw  36210  cdlemd3  36341  cdleme3g  36375  cdleme3h  36376  cdleme7aa  36383  cdleme7d  36387  cdleme7ga  36389  cdleme11c  36402  cdleme15b  36416  cdleme20zN  36442  cdleme20yOLD  36444  cdleme21b  36468  cdleme21c  36469  cdleme21ct  36471  cdleme22b  36483  cdleme32b  36584  cdleme35fnpq  36591  cdleme35f  36596  cdleme36a  36602  cdleme42c  36614  cdleme48bw  36644  cdlemf1  36703  cdlemg2fv2  36742  cdlemg7fvbwN  36749  cdlemg4  36759  cdlemg6c  36762  cdlemg27a  36834  cdlemg27b  36838  cdlemk3  36975  dia2dimlem1  37207  dihord6apre  37399  dihord6b  37403  dihord5apre  37405  dihglbcpreN  37443  dihmeetlem6  37452  dochnel2  37535  dochexmidlem7  37609  lspindp5  37913  mapdh8b  37923  hdmapip0  38061