Theorem mpdan 421

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 19	. 2 |- ( ph -> ph )
2		mpdan.1	. 2 |- ( ph -> ps )
3		mpdan.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpidan  423  mpan2  425  biadanid  618  mpjaodan  805  mpd3an3  1374  eueq2dc  2979  csbiegf  3171  difsnb  3816  reusv3i  4556  fimadmfo  5568  fvmpt3  5725  ffvelcdmd  5783  fnressn  5840  fliftel1  5935  f1oiso2  5968  riota5f  5998  1stvalg  6305  2ndvalg  6306  brtpos2  6417  tfrlemibxssdm  6493  dom2lem  6945  php5  7044  nnfi  7059  xpfi  7124  supisoti  7209  ordiso2  7234  omp1eomlem  7293  nnnninfeq2  7328  onenon  7388  oncardval  7390  cardonle  7391  recidnq  7613  archnqq  7637  prarloclemarch2  7639  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  recexprlemex  7857  0idsr  7987  lep1  9025  suprlubex  9132  uz11  9779  xnegid  10094  eluzfz2  10267  fzsuc  10304  fzsuc2  10314  fzp1disj  10315  fzneuz  10336  fzp1nel  10339  exbtwnzlemex  10509  flhalf  10562  modqval  10586  frec2uzsucd  10663  frecuzrdgsuc  10676  uzsinds  10706  seq3p1  10727  seqp1cd  10732  expubnd  10858  iexpcyc  10906  binom2sub1  10916  hashennn  11042  lswwrd  11160  eqs1  11205  pfxid  11267  wrdind  11303  wrd2ind  11304  pfxccatpfx2  11318  swrdccat3blem  11320  shftfval  11382  shftcan1  11395  cjval  11406  reval  11410  imval  11411  cjmulrcl  11448  addcj  11452  absval  11562  resqrexlemdecn  11573  resqrexlemnmsq  11578  resqrexlemnm  11579  absneg  11611  abscj  11613  sqabsadd  11616  sqabssub  11617  ltabs  11648  dfabsmax  11778  negfi  11789  fsum3  11949  trirecip  12063  fprodseq  12145  efval  12223  ege2le3  12233  efcan  12238  sinval  12264  cosval  12265  efi4p  12279  resin4p  12280  recos4p  12281  sincossq  12310  eirraplem  12339  iddvds  12366  1dvds  12367  bezoutlemstep  12569  coprmgcdb  12661  1idssfct  12688  exprmfct  12711  oddpwdclemdc  12746  phival  12786  odzphi  12820  oddprmdvds  12928  setsn0fun  13120  gsumfzval  13475  0subm  13568  gsumfzz  13579  grprcan  13621  isgrpid2  13624  grpinvid  13644  mulgval  13710  mulgnn0z  13737  0subg  13787  qus0  13823  ghmker  13858  imasabl  13924  mgpplusgg  13939  mgpbasg  13941  mgpscag  13942  mgptsetg  13943  mgpdsg  13945  srgen1zr  14003  opprmulfvalg  14085  opprsllem  14089  1unit  14123  1rinv  14144  subrngmcl  14225  subrg1  14247  subrgmcl  14249  subrgdvds  14251  subrguss  14252  subrginv  14253  subrgdv  14254  subrgunit  14255  subrgugrp  14256  rnrhmsubrg  14268  lmodfopne  14342  lsssn0  14386  lspsn0  14438  lsp0  14439  sralmod  14466  2idlval  14518  cnfldneg  14589  zrhval  14633  cldval  14825  ntrfval  14826  clsfval  14827  neifval  14866  tx1cn  14995  ismet  15070  isxmet  15071  divcnap  15291  dvaddxxbr  15427  dvmulxxbr  15428  dvcoapbr  15433  sgmnncl  15714  1lgs  15774  lgs1  15775  uhgredgiedgb  15987  uhgriedg0edg0  15988  subgrprop3  16115  wlklenvm1  16194  wlklenvm1g  16195  wlkl1loop  16211  wlklenvclwlk  16226  umgrclwwlkge2  16255  clwwlknp  16270  bj-charfun  16405  bj-findis  16577