Theorem mpdan 702

Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
mpdan.1	|- ( ph -> ps )
mpdan.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpdan	|- ( ph -> ch )

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		mpdan.1	. 2 |- ( ph -> ps )
3		mpdan.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpidan  704  mpan2  707  mpjaodan  827  mpd3an3  1425  eueq2  3380  csbiegf  3557  difsnb  4337  reusv3i  4875  fvtresfn  6284  fvmpt3  6286  ffvelrnd  6360  fnressn  6425  fsnex  6538  f1oiso2  6602  riota5f  6636  onsucuni  7028  wfrlem5  7419  seqomlem2  7546  oaordi  7626  nnaordi  7698  qsdisj  7824  dom2lem  7995  canth2g  8114  limenpsi  8135  php4  8147  onfin  8151  sucxpdom  8169  xpfi  8231  dmfi  8244  pwfilem  8260  pwfi  8261  fiin  8328  supiso  8381  ordiso2  8420  wdom2d  8485  infeq5  8534  cantnfp1lem3  8577  cantnflem1d  8585  rankwflemb  8656  onenon  8775  cardonle  8783  sdomsdomcardi  8797  acni  8868  cardaleph  8912  cdaen  8995  cdainf  9014  infcda1  9015  pwsdompw  9026  infdif  9031  cfval  9069  fin34  9212  fin1a2lem1  9222  fin1a2  9237  ttukeylem6  9336  sdomsdomcard  9382  canth3  9383  fpwwe2  9465  canthwelem  9472  gchcda1  9478  pwfseqlem4  9484  gchcdaidm  9490  gchxpidm  9491  tskwe2  9595  rankcf  9599  tskuni  9605  gruxp  9629  dmrecnq  9790  lterpq  9792  archnq  9802  reclem3pr  9871  reclem4pr  9872  0idsr  9918  lep1  10862  ledivp1  10925  negfi  10971  supaddc  10990  supmul1  10992  suprzcl  11457  uz11  11710  zmin  11784  zbtwnre  11786  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  xnegid  12069  xrsupss  12139  xrinfmss  12140  supxrre  12157  infxrre  12166  eluzfz2  12349  fzsuc  12388  fzsuc2  12398  fzp1disj  12399  fzneuz  12421  nn0p1elfzo  12510  fllep1  12602  fraclt1  12603  fracle1  12604  fracge0  12605  flhalf  12631  ceige  12644  ceim1l  12646  fldiv  12659  modval  12670  suppssfz  12794  seqeq1  12804  expubnd  12921  iexpcyc  12969  binom2sub1  12982  faclbnd4lem3  13082  swrdid  13428  swrdccat3blem  13495  cshwn  13543  cshimadifsn  13575  cshimadifsn0  13576  trclexlem  13733  shftfval  13810  shftcan1  13823  reval  13846  cjmulrcl  13884  addcj  13888  absval  13978  absneg  14017  abscj  14019  sqabsadd  14022  sqabssub  14023  leabs  14039  sqreulem  14099  lo1res  14290  o1of2  14343  o1rlimmul  14349  flo1  14586  trirecip  14595  efcan  14826  efi4p  14867  resin4p  14868  recos4p  14869  sincossq  14906  ruclem10  14968  iddvds  14995  1dvds  14996  2ebits  15169  lcmftp  15349  coprmgcdb  15362  1idssfct  15393  exprmfct  15416  eulerthlem2  15487  odzphi  15501  pcprendvds  15545  pcmpt  15596  vdwlem8  15692  0ram2  15725  prmgaplem7  15761  setsn0fun  15895  setsexstruct2  15897  pwsvscaval  16155  issect2  16414  2initoinv  16660  initoeu1  16661  initoeu2lem1  16664  initoeu2  16666  2termoinv  16667  termoeu1  16668  homarel  16686  joinfval  17001  meetfval  17015  latjcom  17059  latmcom  17075  sgrp2nmndlem5  17416  grprcan  17455  isgrpid2  17458  grpinvid  17476  mulgnn0z  17567  0subg  17619  qus0  17652  ghmker  17686  symginv  17822  pmtrfrn  17878  odmulg2  17972  slwpgp  18028  pj1eq  18113  efgtf  18135  frgpinv  18177  frgpup2  18189  mulgnn0di  18231  cnaddablx  18271  cnaddabl  18272  zaddablx  18275  dprdfadd  18419  dpjidcl  18457  dpjlid  18460  pgpfac1lem3  18476  srgen1zr  18530  ringlz  18587  ringrz  18588  1unit  18658  unitgrpid  18669  1rinv  18679  irredn0  18703  irredneg  18710  isdrng2  18757  abv0  18831  abv1z  18832  abvneg  18834  lmodfopne  18901  lsssn0  18948  lspsn0  19008  lsp0  19009  lmhmvsca  19045  lmhmrnlss  19050  lmhmkerlss  19051  lsppratlem5  19151  rsp1  19224  ringen1zr  19277  rlmassa  19326  snifpsrbag  19366  psrvscaval  19392  psrdi  19406  psrdir  19407  mplsubglem  19434  mplvscaval  19448  coe1sclmulfv  19653  ply1idvr1  19663  evl1var  19700  cnfldneg  19772  zringcyg  19839  chrid  19875  chrrhm  19879  ip0r  19982  ocvlss  20016  ocv1  20023  mamuvs1  20211  mamuvs2  20212  matecl  20231  matvscacell  20242  mat0scmat  20344  submaval0  20386  mdetrsca  20409  maduval  20444  minmar1val0  20453  pmatcollpw3fi1lem2  20592  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chcoeffeqlem  20690  cayleyhamilton0  20694  cayleyhamiltonALT  20696  toponsspwpw  20726  cctop  20810  cldval  20827  ntrfval  20828  clsfval  20829  cmclsopn  20866  opncldf3  20890  neifval  20903  lpfval  20942  cnrmnrm  21165  islocfin  21320  tx1cn  21412  idqtop  21509  kqtopon  21530  kqid  21531  kqcld  21538  hmphen2  21602  filssufil  21716  ufileu  21723  alexsublem  21848  symgtgp  21905  ustuqtop4  22048  cstucnd  22088  metustexhalf  22361  nm0  22433  rlmnlm  22492  nmolb  22521  metdseq0  22657  pi1xfrval  22854  clmvneg1  22899  clmvsubval  22909  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  cmetcaulem  23086  ovolicc2lem3  23287  ovolicc2lem4  23288  mbfmulc2lem  23414  i1fpos  23473  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  itg2ge0  23502  dvres2  23676  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvfsumlem4  23792  ftc1a  23800  ftc1lem6  23804  uc1pmon1p  23911  ig1pval2  23933  dgradd2  24024  dgrcolem2  24030  plydivlem4  24051  plydiveu  24053  elqaalem3  24076  qaa  24078  ulmdvlem1  24154  abelthlem6  24190  abelthlem7  24192  eflogeq  24348  jensenlem2  24714  harmonicbnd4  24737  sgmnncl  24873  dchrptlem2  24990  1lgs  25065  lgs1  25066  dchrisumlem2  25179  dchrisum0lem2a  25206  selberg2lem  25239  pntrsumo1  25254  pntrsumbnd  25255  pntpbnd1  25275  pntlemr  25291  pntlemj  25292  padicabvf  25320  istrkg3ld  25360  incistruhgr  25974  subgrprop3  26168  subgruhgredgd  26176  usgrexi  26337  cusgrexi  26339  cusgrsizeinds  26348  vtxdgfusgrf  26393  1hevtxdg1  26402  1egrvtxdg1  26405  ewlkprop  26499  wlklenvm1  26517  wlkl1loop  26534  wlkp1lem4  26573  2pthnloop  26627  upgrclwlkcompim  26677  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  crctcshwlkn0lem7  26708  crctcshlem4  26712  wspthnonp  26744  wlkpwwlkf1ouspgr  26765  wwlksnwwlksnon  26810  umgr2wlkon  26846  elwwlks2ons3  26848  elwspths2spth  26862  umgrclwwlksge2  26912  wwlksubclwwlks  26925  erclwwlksref  26934  erclwwlksnref  26946  0pthon1  26989  1wlkdlem4  27000  1pthd  27003  3spthd  27036  eupth2eucrct  27077  eucrctshift  27103  eucrct2eupth  27105  frgrncvvdeqlem8  27170  frgr2wwlkeqm  27195  isgrpoi  27352  grpoinvfval  27376  grpodivfval  27388  vcz  27430  cnaddabloOLD  27436  nvz0  27523  sspz  27590  lno0  27611  nmobndi  27630  ipasslem2  27687  shunssi  28227  ococin  28267  ssjo  28306  pjocini  28557  nlfnval  28740  lncnopbd  28896  riesz3i  28921  cnlnadjlem7  28932  pjclem4  29058  pj3si  29066  hstoc  29081  hstnmoc  29082  hstoh  29091  hst0  29092  mdsl2i  29181  chirredlem3  29251  chirredlem4  29252  dmdbr5ati  29281  rexunirn  29331  fcnvgreu  29472  infxrge0glb  29530  2sqcoprm  29647  omndmul2  29712  omndmul  29714  isarchi3  29741  orng0le1  29812  esumcvg  30148  esumcvgre  30153  sigaval  30173  unelldsys  30221  fiunelros  30237  measval  30261  pmeasmono  30386  eulerpartlemgvv  30438  probfinmeasb  30491  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsi  30576  ballotlemfrci  30589  sgnneg  30602  signlem0  30664  breprexp  30711  bnj1006  31029  bnj1110  31050  bnj1253  31085  bnj1280  31088  bnj1463  31123  bnj1312  31126  erdszelem7  31179  erdszelem8  31180  cvmliftlem10  31276  cvmliftlem13  31278  cvmlift2lem9  31293  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  dfrdg2  31701  dftrpred3g  31733  frrlem5  31784  bdayval  31801  noextendgt  31823  nosupbnd2lem1  31861  cldregopn  32326  tailfval  32367  filnetlem3  32375  filnetlem4  32376  ontopbas  32427  f1omptsnlem  33183  icoreunrn  33207  relowlpssretop  33212  wl-sbal2  33347  unccur  33392  poimirlem1  33410  poimirlem2  33411  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem28  33437  poimir  33442  ismblfin  33450  cnambfre  33458  bddiblnc  33480  ftc1cnnc  33484  dvasin  33496  ismtyres  33607  heiborlem8  33617  ghomidOLD  33688  rngolz  33721  rngorz  33722  rngosn6  33725  rngonegmn1l  33740  rngonegmn1r  33741  rngoneglmul  33742  rngonegrmul  33743  idlnegcl  33821  0idl  33824  0rngo  33826  keridl  33831  smprngopr  33851  lshpne0  34273  lkrval  34375  ldualvaddval  34418  ldualvsval  34425  opoc1  34489  pmap0  35051  pmap1N  35053  pexmidALTN  35264  cdleme31fv  35678  cdlemg27b  35984  erngdvlem4  36279  erng0g  36282  erngdvlem4-rN  36287  dvalveclem  36314  dvh0g  36400  dih0cnv  36572  dih1rn  36576  dih1cnv  36577  doch0  36647  doch1  36648  lcfl7lem  36788  mapdheq  37017  hdmap1eq  37091  hdmapval2lem  37123  hgmapvvlem3  37217  mzpval  37295  mzpindd  37309  pellex  37399  2nn0ind  37510  jm2.26lem3  37568  pw2f1o2val  37606  wepwsolem  37612  fnwe2lem3  37622  lnmfg  37652  dgrsub2  37705  mpaaeu  37720  flcidc  37744  rtrclexlem  37923  cnvrcl0  37932  brcoffn  38328  clsk1indlem3  38341  clsneif1o  38402  clsneicnv  38403  clsneikex  38404  clsneinex  38405  neicvgmex  38415  neicvgel1  38417  suprleubrd  38466  suprlubrd  38470  imo72b2  38475  dvconstbi  38533  bcc0  38539  binomcxplemnotnn0  38555  nnfoctb  39213  infleinflem1  39586  fprodcnlem  39831  sumnnodd  39862  icccncfext  40100  itgsin0pilem1  40165  stoweidlem22  40239  stoweidlem32  40249  stoweidlem35  40252  stoweidlem36  40253  stoweidlem37  40254  stoweidlem43  40260  stoweidlem50  40267  wallispilem5  40286  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem8  40298  stirlinglem11  40301  stirlinglem12  40302  stirlinglem14  40304  stirlinglem15  40305  fourierdlem11  40335  fourierdlem20  40344  fourierdlem21  40345  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem64  40387  fourierdlem71  40394  fourierdlem79  40402  fourierdlem90  40413  fourierdlem91  40414  fourierswlem  40447  etransclem17  40468  etransclem38  40489  saluni  40544  meaiininclem  40700  issmflelem  40953  issmfgtlem  40964  issmfgelem  40977  smflimsuplem4  41029  pfxid  41392  pfx2  41412  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  sprval  41729  isclintop  41843  clintopcllaw  41847  nzrneg1ne0  41869  rnglz  41884  c0snmgmhm  41914  zrrnghm  41917  lidldomn1  41921  uzlidlring  41929  2zrngnmlid  41949  cznrng  41955  zrinitorngc  42000  zrtermorngc  42001  zrtermoringc  42070  coe1id  42172  blenre  42368  blennn  42369  onsetreclem2  42449