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  4803  po3nr  4804  ordn2lp  4888  onssneli  4977  tfi  6673  nnlim  6698  smoord  7038  tz7.48-3  7111  oalimcl  7211  omlimcl  7229  oneo  7232  omopth2  7235  nnneo  7302  mapdom2  7690  php3  7705  onomeneq  7709  sucdom2  7716  isfinite2  7780  domunfican  7795  ordtypelem7  7952  unxpwdom2  8017  cantnfp1lem2  8101  oemapvali  8106  cantnflem1  8111  cantnflem2  8112  cantnfp1lem2OLD  8127  cantnflem1OLD  8134  rankpwi  8244  tskwe  8334  alephordi  8458  alephdom  8465  cardaleph  8473  cflim2  8646  isfin4-3  8698  fin23lem26  8708  fin1a2lem13  8795  axcclem  8840  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwe2  9024  pwxpndom2  9046  pwxpndom  9047  pwcdandom  9048  gchaleph  9052  r1wunlim  9118  inatsk  9159  tskuni  9164  gruina  9199  prlem934  9414  dedekind  9747  qextltlem  11411  ixxub  11560  ixxlb  11561  seqf1olem1  12127  facndiv  12347  cnpart  13054  rlimuni  13354  rlimcld2  13382  isercoll  13471  incexclem  13629  isumltss  13641  alzdvds  14017  fzm1ndvds  14019  fzo0dvdseq  14020  bitsfzolem  14065  smuval2  14113  smupvallem  14114  bezoutlem3  14159  rpdvds  14246  nonsq  14273  prmdiv  14296  odzdvds  14303  pcprendvds  14345  pcprendvds2  14346  pcpremul  14348  pcdvdsb  14373  pcadd2  14390  pockthlem  14404  prmreclem5  14419  prmreclem6  14420  1arith  14426  4sqlem11  14454  vdwlem11  14490  vdwlem12  14491  ramubcl  14517  mrissmrcd  15018  pltnlt  15576  acsfiindd  15785  odcl2  16565  gexnnod  16586  pgpssslw  16612  torsubg  16838  lt6abl  16875  ablfacrplem  17094  pgpfac1lem3  17106  irredrmul  17334  islbs3  17779  lbsextlem3  17784  lbsextlem4  17785  rng1nfld  17904  mvrf1  18059  f1lindf  18834  perfopn  19663  pnfnei  19698  mnfnei  19699  haust1  19830  cmpcld  19879  ptbasfi  20059  fbncp  20317  isfild  20336  fbasfip  20346  filufint  20398  rnelfmlem  20430  fmfnfm  20436  fclscf  20503  ptcmplem3  20531  opnsubg  20583  bldisj  20878  iccntr  21303  icccmplem2  21305  reconnlem1  21308  reconnlem2  21309  evth  21436  lebnumlem3  21440  ovolicc2lem3  21907  volfiniun  21934  iundisj  21935  dvne0  22389  lhop2  22393  itgsubstlem  22426  coemullem  22623  plyexmo  22685  wilthlem2  23319  wilth  23321  mumul  23431  chtublem  23462  perfect1  23479  lgsdilem2  23582  lgsne0  23584  lgsqrlem2  23593  lgseisenlem1  23600  lgseisenlem2  23601  lgsquadlem1  23605  lgsquadlem2  23606  lgsquadlem3  23607  lgsquad2lem1  23609  2sqblem  23628  chebbnd1lem1  23630  pntpbnd2  23748  pntlem3  23770  ostth  23800  vdgr1a  24882  chirredlem1  27285  iundisjf  27424  ofpreima2  27484  iundisjfi  27577  logccne0  27989  lgamgulmlem1  28548  fundmpss  29171  dfon2lem4  29193  dfon2lem7  29196  sltval2  29391  sltasym  29407  broutsideof2  29747  outsidele  29757  onint1  29889  fin2so  30015  nn0prpwlem  30115  nn0prpw  30116  pellexlem6  30745  elpell14qr2  30773  pellfundglb  30796  jm2.19  30910  jm2.26lem3  30918  setindtr  30941  harinf  30951  dgraa0p  31074  lpssat  34478  exatleN  34868  3noncolr2  34913  4noncolr3  34917  3dimlem3  34925  3dimlem3OLDN  34926  3dimlem4a  34927  3dimlem4  34928  3dimlem4OLDN  34929  3atlem4  34950  3atlem5  34951  3atlem6  34952  llnnleat  34977  lplnnle2at  35005  lvolnle3at  35046  4atlem0a  35057  4atlem0ae  35058  dalem21  35158  dalem54  35190  cdlemblem  35257  lhpmcvr4N  35490  4atexlemnclw  35534  cdlemd3  35665  cdleme3g  35699  cdleme3h  35700  cdleme7aa  35707  cdleme7d  35711  cdleme7ga  35713  cdleme11c  35726  cdleme15b  35740  cdleme20zN  35766  cdleme20yOLD  35768  cdleme21b  35792  cdleme21c  35793  cdleme21ct  35795  cdleme22b  35807  cdleme32b  35908  cdleme35fnpq  35915  cdleme35f  35920  cdleme36a  35926  cdleme42c  35938  cdleme48bw  35968  cdlemf1  36027  cdlemg2fv2  36066  cdlemg7fvbwN  36073  cdlemg4  36083  cdlemg6c  36086  cdlemg27a  36158  cdlemg27b  36162  cdlemk3  36299  dia2dimlem1  36531  dihord6apre  36723  dihord6b  36727  dihord5apre  36729  dihglbcpreN  36767  dihmeetlem6  36776  dochnel2  36859  dochexmidlem7  36933  lspindp5  37237  mapdh8b  37247  hdmapip0  37385