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  4675  po3nr  4676  ordn2lp  4760  onssneli  4849  tfi  6485  nnlim  6510  smoord  6847  tz7.48-3  6920  oalimcl  7020  omlimcl  7038  oneo  7041  omopth2  7044  nnneo  7111  mapdom2  7503  php3  7518  onomeneq  7521  sucdom2  7528  isfinite2  7591  domunfican  7605  ordtypelem7  7759  unxpwdom2  7824  cantnfp1lem2  7908  oemapvali  7913  cantnflem1  7918  cantnflem2  7919  cantnfp1lem2OLD  7934  cantnflem1OLD  7941  rankpwi  8051  tskwe  8141  alephordi  8265  alephdom  8272  cardaleph  8280  cflim2  8453  isfin4-3  8505  fin23lem26  8515  fin1a2lem13  8602  axcclem  8647  fpwwe2lem12  8829  fpwwe2lem13  8830  fpwwe2  8831  pwxpndom2  8853  pwxpndom  8854  pwcdandom  8855  gchaleph  8859  r1wunlim  8925  inatsk  8966  tskuni  8971  gruina  9006  prlem934  9223  dedekind  9554  qextltlem  11193  ixxub  11342  ixxlb  11343  seqf1olem1  11866  facndiv  12085  cnpart  12750  rlimuni  13049  rlimcld2  13077  isercoll  13166  incexclem  13320  isumltss  13332  alzdvds  13604  fzm1ndvds  13606  fzo0dvdseq  13607  bitsfzolem  13651  smuval2  13699  smupvallem  13700  bezoutlem3  13745  rpdvds  13831  nonsq  13858  prmdiv  13881  odzdvds  13888  pcprendvds  13928  pcprendvds2  13929  pcpremul  13931  pcdvdsb  13956  pcadd2  13973  pockthlem  13987  prmreclem5  14002  prmreclem6  14003  1arith  14009  4sqlem11  14037  vdwlem11  14073  vdwlem12  14074  ramubcl  14100  mrissmrcd  14599  pltnlt  15159  acsfiindd  15368  odcl2  16087  gexnnod  16108  pgpssslw  16134  torsubg  16357  lt6abl  16392  ablfacrplem  16588  pgpfac1lem3  16600  irredrmul  16821  islbs3  17258  lbsextlem3  17263  lbsextlem4  17264  mvrf1  17520  f1lindf  18273  perfopn  18811  pnfnei  18846  mnfnei  18847  haust1  18978  cmpcld  19027  ptbasfi  19176  fbncp  19434  isfild  19453  fbasfip  19463  filufint  19515  rnelfmlem  19547  fmfnfm  19553  fclscf  19620  ptcmplem3  19648  opnsubg  19700  bldisj  19995  iccntr  20420  icccmplem2  20422  reconnlem1  20425  reconnlem2  20426  evth  20553  lebnumlem3  20557  ovolicc2lem3  21024  volfiniun  21050  iundisj  21051  dvne0  21505  lhop2  21509  itgsubstlem  21542  coemullem  21739  plyexmo  21801  wilthlem2  22429  wilth  22431  mumul  22541  chtublem  22572  perfect1  22589  lgsdilem2  22692  lgsne0  22694  lgsqrlem2  22703  lgseisenlem1  22710  lgseisenlem2  22711  lgsquadlem1  22715  lgsquadlem2  22716  lgsquadlem3  22717  lgsquad2lem1  22719  2sqblem  22738  chebbnd1lem1  22740  pntpbnd2  22858  pntlem3  22880  ostth  22910  vdgr1a  23598  chirredlem1  25816  iundisjf  25953  iundisjfi  26102  logccne0  26477  lgamgulmlem1  27037  fundmpss  27599  dfon2lem4  27621  dfon2lem7  27624  sltval2  27819  sltasym  27835  broutsideof2  28175  outsidele  28185  onint1  28317  fin2so  28442  nn0prpwlem  28543  nn0prpw  28544  pellexlem6  29201  elpell14qr2  29229  pellfundglb  29252  jm2.19  29368  jm2.26lem3  29376  setindtr  29399  harinf  29409  dgraa0p  29532  rng1nfld  31024  lpssat  32754  exatleN  33144  3noncolr2  33189  4noncolr3  33193  3dimlem3  33201  3dimlem3OLDN  33202  3dimlem4a  33203  3dimlem4  33204  3dimlem4OLDN  33205  3atlem4  33226  3atlem5  33227  3atlem6  33228  llnnleat  33253  lplnnle2at  33281  lvolnle3at  33322  4atlem0a  33333  4atlem0ae  33334  dalem21  33434  dalem54  33466  cdlemblem  33533  lhpmcvr4N  33766  4atexlemnclw  33810  cdlemd3  33940  cdleme3g  33974  cdleme3h  33975  cdleme7aa  33982  cdleme7d  33986  cdleme7ga  33988  cdleme11c  34001  cdleme15b  34015  cdleme20zN  34041  cdleme20y  34042  cdleme21b  34066  cdleme21c  34067  cdleme21ct  34069  cdleme22b  34081  cdleme32b  34182  cdleme35fnpq  34189  cdleme35f  34194  cdleme36a  34200  cdleme42c  34212  cdleme48bw  34242  cdlemf1  34301  cdlemg2fv2  34340  cdlemg7fvbwN  34347  cdlemg4  34357  cdlemg6c  34360  cdlemg27a  34432  cdlemg27b  34436  cdlemk3  34573  dia2dimlem1  34805  dihord6apre  34997  dihord6b  35001  dihord5apre  35003  dihglbcpreN  35041  dihmeetlem6  35050  dochnel2  35133  dochexmidlem7  35207  lspindp5  35511  mapdh8b  35521  hdmapip0  35659