Theorem mtod 170

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 23	. 2 |- ( ph -> ( ps -> -. ch ) )
4	1, 3	pm2.65d 168	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  mtoi  171  mtbid  292  mtbird  293  mtand  641  mtord  642  po2nr  4476  po3nr  4477  ordn2lp  4561  onssneli  4650  tfi  4792  nnlim  4817  smoord  6586  tz7.48-3  6660  oalimcl  6762  omlimcl  6780  oneo  6783  omopth2  6786  nnneo  6853  mapdom2  7237  php3  7252  onomeneq  7255  sucdom2  7262  isfinite2  7324  domunfican  7338  ordtypelem7  7449  unxpwdom2  7512  cantnfp1lem2  7591  oemapvali  7596  cantnflem1  7601  cantnflem2  7602  rankpwi  7705  tskwe  7793  alephordi  7911  alephdom  7918  cardaleph  7926  cflim2  8099  isfin4-3  8151  fin23lem26  8161  fin1a2lem13  8248  axcclem  8293  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  pwxpndom2  8496  pwxpndom  8497  pwcdandom  8498  gchaleph  8506  r1wunlim  8568  inatsk  8609  tskuni  8614  gruina  8649  prlem934  8866  qextltlem  10744  ixxub  10893  ixxlb  10894  seqf1olem1  11317  facndiv  11534  cnpart  12000  rlimuni  12299  rlimcld2  12327  isercoll  12416  incexclem  12571  isumltss  12583  alzdvds  12854  fzm1ndvds  12856  fzo0dvdseq  12857  bitsfzolem  12901  smuval2  12949  smupvallem  12950  bezoutlem3  12995  rpdvds  13079  nonsq  13106  prmdiv  13129  odzdvds  13136  pcprendvds  13169  pcprendvds2  13170  pcpremul  13172  pcdvdsb  13197  pcadd2  13214  pockthlem  13228  prmreclem5  13243  prmreclem6  13244  1arith  13250  4sqlem11  13278  vdwlem11  13314  vdwlem12  13315  ramubcl  13341  mrissmrcd  13820  pltnlt  14380  acsfiindd  14558  odcl2  15156  gexnnod  15177  pgpssslw  15203  torsubg  15424  lt6abl  15459  ablfacrplem  15578  pgpfac1lem3  15590  irredrmul  15767  islbs3  16182  lbsextlem3  16187  lbsextlem4  16188  mvrf1  16444  perfopn  17203  pnfnei  17238  mnfnei  17239  haust1  17370  cmpcld  17419  ptbasfi  17566  fbncp  17824  isfild  17843  fbasfip  17853  filufint  17905  rnelfmlem  17937  fmfnfm  17943  fclscf  18010  ptcmplem3  18038  opnsubg  18090  bldisj  18381  iccntr  18805  icccmplem2  18807  reconnlem1  18810  reconnlem2  18811  evth  18937  lebnumlem3  18941  ovolicc2lem3  19368  volfiniun  19394  iundisj  19395  dvne0  19848  lhop2  19852  itgsubstlem  19885  coemullem  20121  plyexmo  20183  wilthlem2  20805  wilth  20807  mumul  20917  chtublem  20948  perfect1  20965  lgsdilem2  21068  lgsne0  21070  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem1  21095  2sqblem  21114  chebbnd1lem1  21116  pntpbnd2  21234  pntlem3  21256  ostth  21286  vdgr1a  21630  chirredlem1  23846  iundisjf  23982  iundisjfi  24105  logccne0  24349  lgamgulmlem1  24766  dedekind  25140  fundmpss  25336  dfon2lem4  25356  dfon2lem7  25359  sltval2  25524  sltasym  25540  broutsideof2  25960  outsidele  25970  onint1  26103  nn0prpwlem  26215  nn0prpw  26216  pellexlem6  26787  elpell14qr2  26815  pellfundglb  26838  jm2.19  26954  jm2.26lem3  26962  setindtr  26985  harinf  26995  f1lindf  27160  dgraa0p  27222  lpssat  29496  exatleN  29886  3noncolr2  29931  4noncolr3  29935  3dimlem3  29943  3dimlem3OLDN  29944  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  3atlem4  29968  3atlem5  29969  3atlem6  29970  llnnleat  29995  lplnnle2at  30023  lvolnle3at  30064  4atlem0a  30075  4atlem0ae  30076  dalem21  30176  dalem54  30208  cdlemblem  30275  lhpmcvr4N  30508  4atexlemnclw  30552  cdlemd3  30682  cdleme3g  30716  cdleme3h  30717  cdleme7aa  30724  cdleme7d  30728  cdleme7ga  30730  cdleme11c  30743  cdleme15b  30757  cdleme20zN  30783  cdleme20y  30784  cdleme21b  30808  cdleme21c  30809  cdleme21ct  30811  cdleme22b  30823  cdleme32b  30924  cdleme35fnpq  30931  cdleme35f  30936  cdleme36a  30942  cdleme42c  30954  cdleme48bw  30984  cdlemf1  31043  cdlemg2fv2  31082  cdlemg7fvbwN  31089  cdlemg4  31099  cdlemg6c  31102  cdlemg27a  31174  cdlemg27b  31178  cdlemk3  31315  dia2dimlem1  31547  dihord6apre  31739  dihord6b  31743  dihord5apre  31745  dihglbcpreN  31783  dihmeetlem6  31792  dochnel2  31875  dochexmidlem7  31949  lspindp5  32253  mapdh8b  32263  hdmapip0  32401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8