Theorem mtod 180

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 26	. 2 |- ( ph -> ( ps -> -. ch ) )
4	1, 3	pm2.65d 178	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  181  mtbid  301  mtbird  302  mtand  663  mtord  664  po2nr  4788  po3nr  4789  ordn2lp  5462  onssneli  5551  tfi  6694  nnlim  6719  smoord  7092  tz7.48-3  7169  oalimcl  7269  omlimcl  7287  oneo  7290  omopth2  7293  nnneo  7360  mapdom2  7749  php3  7764  onomeneq  7768  sucdom2  7774  isfinite2  7835  domunfican  7850  ordtypelem7  8039  unxpwdom2  8103  cantnfp1lem2  8183  oemapvali  8188  cantnflem1  8193  cantnflem2  8194  rankpwi  8293  tskwe  8383  alephordi  8503  alephdom  8510  cardaleph  8518  cflim2  8691  isfin4-3  8743  fin23lem26  8753  fin1a2lem13  8840  axcclem  8885  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  pwxpndom2  9089  pwxpndom  9090  pwcdandom  9091  gchaleph  9095  r1wunlim  9161  inatsk  9202  tskuni  9207  gruina  9242  prlem934  9457  dedekind  9796  qextltlem  11495  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  seqf1olem1  12249  facndiv  12470  cnpart  13282  rlimuni  13592  rlimcld2  13620  isercoll  13709  incexclem  13872  isumltss  13884  alzdvds  14333  fzm1ndvds  14335  fzo0dvdseq  14336  bitsfzolem  14382  smuval2  14430  smupvallem  14431  bezoutlem3  14479  rpdvds  14647  nonsq  14679  prmdiv  14702  odzdvds  14709  pcprendvds  14753  pcprendvds2  14754  pcpremul  14756  pcdvdsb  14781  pcadd2  14798  pockthlem  14812  prmreclem5  14827  prmreclem6  14828  1arith  14834  4sqlem11  14862  vdwlem11  14904  vdwlem12  14905  ramubcl  14939  mrissmrcd  15497  pltnlt  16165  acsfiindd  16374  odcl2  17154  gexnnod  17175  pgpssslw  17201  torsubg  17427  lt6abl  17464  ablfacrplem  17633  pgpfac1lem3  17645  irredrmul  17870  islbs3  18313  lbsextlem3  18318  lbsextlem4  18319  rng1nfld  18437  mvrf1  18584  f1lindf  19311  perfopn  20132  pnfnei  20167  mnfnei  20168  haust1  20299  cmpcld  20348  ptbasfi  20527  fbncp  20785  isfild  20804  fbasfip  20814  filufint  20866  rnelfmlem  20898  fmfnfm  20904  fclscf  20971  ptcmplem3  21000  opnsubg  21053  bldisj  21344  iccntr  21750  icccmplem2  21752  reconnlem1  21755  reconnlem2  21756  evth  21883  lebnumlem3  21887  ovolicc2lem3  22350  volfiniun  22377  iundisj  22378  dvne0  22840  lhop2  22844  itgsubstlem  22877  coemullem  23072  plyexmo  23134  logccne0  23393  lgamgulmlem1  23819  wilthlem2  23859  wilth  23861  mumul  23971  chtublem  24002  perfect1  24019  lgsdilem2  24122  lgsne0  24124  lgsqrlem2  24133  lgseisenlem1  24140  lgseisenlem2  24141  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  lgsquad2lem1  24149  2sqblem  24168  chebbnd1lem1  24170  pntpbnd2  24288  pntlem3  24310  ostth  24340  vdgr1a  25479  chirredlem1  27878  iundisjf  28038  ofpreima2  28109  iundisjfi  28208  fundmpss  30194  dfon2lem4  30219  dfon2lem7  30222  sltval2  30330  sltasym  30346  broutsideof2  30674  outsidele  30684  nn0prpwlem  30763  nn0prpw  30764  onint1  30894  fin2so  31635  poimirlem16  31659  lpssat  32287  exatleN  32677  3noncolr2  32722  4noncolr3  32726  3dimlem3  32734  3dimlem3OLDN  32735  3dimlem4a  32736  3dimlem4  32737  3dimlem4OLDN  32738  3atlem4  32759  3atlem5  32760  3atlem6  32761  llnnleat  32786  lplnnle2at  32814  lvolnle3at  32855  4atlem0a  32866  4atlem0ae  32867  dalem21  32967  dalem54  32999  cdlemblem  33066  lhpmcvr4N  33299  4atexlemnclw  33343  cdlemd3  33474  cdleme3g  33508  cdleme3h  33509  cdleme7aa  33516  cdleme7d  33520  cdleme7ga  33522  cdleme11c  33535  cdleme15b  33549  cdleme20zN  33575  cdleme20yOLD  33577  cdleme21b  33601  cdleme21c  33602  cdleme21ct  33604  cdleme22b  33616  cdleme32b  33717  cdleme35fnpq  33724  cdleme35f  33729  cdleme36a  33735  cdleme42c  33747  cdleme48bw  33777  cdlemf1  33836  cdlemg2fv2  33875  cdlemg7fvbwN  33882  cdlemg4  33892  cdlemg6c  33895  cdlemg27a  33967  cdlemg27b  33971  cdlemk3  34108  dia2dimlem1  34340  dihord6apre  34532  dihord6b  34536  dihord5apre  34538  dihglbcpreN  34576  dihmeetlem6  34585  dochnel2  34668  dochexmidlem7  34742  lspindp5  35046  mapdh8b  35056  hdmapip0  35194  pellexlem6  35387  elpell14qr2  35415  pellfundglb  35438  jm2.19  35553  jm2.26lem3  35561  setindtr  35584  harinf  35594  dgraa0p  35713