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  nn0p1elfzo  10422  exbtwnzlemex  10510  flhalf  10563  modqval  10587  frec2uzsucd  10664  frecuzrdgsuc  10677  uzsinds  10707  seq3p1  10728  seqp1cd  10733  expubnd  10859  iexpcyc  10907  binom2sub1  10917  hashennn  11043  lswwrd  11164  eqs1  11209  pfxid  11271  wrdind  11307  wrd2ind  11308  pfxccatpfx2  11322  swrdccat3blem  11324  shftfval  11386  shftcan1  11399  cjval  11410  reval  11414  imval  11415  cjmulrcl  11452  addcj  11456  absval  11566  resqrexlemdecn  11577  resqrexlemnmsq  11582  resqrexlemnm  11583  absneg  11615  abscj  11617  sqabsadd  11620  sqabssub  11621  ltabs  11652  dfabsmax  11782  negfi  11793  fsum3  11953  trirecip  12067  fprodseq  12149  efval  12227  ege2le3  12237  efcan  12242  sinval  12268  cosval  12269  efi4p  12283  resin4p  12284  recos4p  12285  sincossq  12314  eirraplem  12343  iddvds  12370  1dvds  12371  bezoutlemstep  12573  coprmgcdb  12665  1idssfct  12692  exprmfct  12715  oddpwdclemdc  12750  phival  12790  odzphi  12824  oddprmdvds  12932  setsn0fun  13124  gsumfzval  13479  0subm  13572  gsumfzz  13583  grprcan  13625  isgrpid2  13628  grpinvid  13648  mulgval  13714  mulgnn0z  13741  0subg  13791  qus0  13827  ghmker  13862  imasabl  13928  mgpplusgg  13943  mgpbasg  13945  mgpscag  13946  mgptsetg  13947  mgpdsg  13949  srgen1zr  14007  opprmulfvalg  14089  opprsllem  14093  1unit  14127  1rinv  14148  subrngmcl  14229  subrg1  14251  subrgmcl  14253  subrgdvds  14255  subrguss  14256  subrginv  14257  subrgdv  14258  subrgunit  14259  subrgugrp  14260  rnrhmsubrg  14272  lmodfopne  14346  lsssn0  14390  lspsn0  14442  lsp0  14443  sralmod  14470  2idlval  14522  cnfldneg  14593  zrhval  14637  cldval  14829  ntrfval  14830  clsfval  14831  neifval  14870  tx1cn  14999  ismet  15074  isxmet  15075  divcnap  15295  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  sgmnncl  15718  1lgs  15778  lgs1  15779  uhgredgiedgb  15991  uhgriedg0edg0  15992  subgrprop3  16119  wlklenvm1  16198  wlklenvm1g  16199  wlkl1loop  16215  wlklenvclwlk  16230  umgrclwwlkge2  16259  clwwlknp  16274  bj-charfun  16428  bj-findis  16600