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  806  mpd3an3  1375  eueq2dc  2993  csbiegf  3185  difsnb  3842  reusv3i  4585  fimadmfo  5604  fvmpt3  5761  ffvelcdmd  5818  fnressn  5875  fliftel1  5973  f1oiso2  6006  riota5f  6038  1stvalg  6349  2ndvalg  6350  brtpos2  6495  tfrlemibxssdm  6571  dom2lem  7024  php5  7125  nnfi  7140  xpfi  7205  supisoti  7314  ordiso2  7339  omp1eomlem  7398  nnnninfeq2  7433  onenon  7493  oncardval  7495  cardonle  7496  recidnq  7724  archnqq  7748  prarloclemarch2  7750  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  recexprlemex  7968  0idsr  8098  lep1  9136  suprlubex  9243  uz11  9895  xnegid  10211  eluzfz2  10386  fzsuc  10424  fzsuc2  10435  fzp1disj  10436  fzneuz  10457  fzp1nel  10460  nn0p1elfzo  10543  exbtwnzlemex  10633  flhalf  10686  modqval  10710  frec2uzsucd  10787  frecuzrdgsuc  10800  uzsinds  10830  seq3p1  10851  seqp1cd  10856  expubnd  10982  iexpcyc  11030  binom2sub1  11040  hashennn  11168  lswwrd  11296  eqs1  11341  pfxid  11403  wrdind  11439  wrd2ind  11440  pfxccatpfx2  11454  swrdccat3blem  11456  shftfval  11531  shftcan1  11544  cjval  11555  reval  11559  imval  11560  cjmulrcl  11597  addcj  11601  absval  11711  resqrexlemdecn  11722  resqrexlemnmsq  11727  resqrexlemnm  11728  absneg  11760  abscj  11762  sqabsadd  11765  sqabssub  11766  ltabs  11797  dfabsmax  11927  negfi  11938  fsum3  12098  trirecip  12212  fprodseq  12294  efval  12372  ege2le3  12382  efcan  12387  sinval  12413  cosval  12414  efi4p  12428  resin4p  12429  recos4p  12430  sincossq  12459  eirraplem  12488  iddvds  12515  1dvds  12516  bezoutlemstep  12718  coprmgcdb  12810  1idssfct  12837  exprmfct  12860  oddpwdclemdc  12895  phival  12935  odzphi  12969  oddprmdvds  13077  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsi  13202  ballotfilemfrci  13215  setsn0fun  13333  gsumfzval  13688  0subm  13781  gsumfzz  13792  grprcan  13834  isgrpid2  13837  grpinvid  13857  mulgval  13923  mulgnn0z  13950  0subg  14000  qus0  14036  ghmker  14071  imasabl  14137  mgpplusgg  14152  mgpbasg  14154  mgpscag  14155  mgptsetg  14156  mgpdsg  14158  srgen1zr  14216  opprmulfvalg  14298  opprsllem  14302  1unit  14337  1rinv  14358  subrngmcl  14440  subrg1  14462  subrgmcl  14464  subrgdvds  14466  subrguss  14467  subrginv  14468  subrgdv  14469  subrgunit  14470  subrgugrp  14471  rnrhmsubrg  14483  ringen1zr  14546  lmodfopne  14586  lsssn0  14630  lspsn0  14682  lsp0  14683  sralmod  14710  2idlval  14762  cnfldneg  14833  zrhval  14877  psrbagfsupp  14931  cldval  15076  ntrfval  15077  clsfval  15078  neifval  15117  tx1cn  15246  ismet  15321  isxmet  15322  divcnap  15542  dvaddxxbr  15678  dvmulxxbr  15679  dvcoapbr  15684  sgmnncl  15968  1lgs  16028  lgs1  16029  uhgredgiedgb  16241  uhgriedg0edg0  16242  subgrprop3  16369  wlklenvm1  16448  wlklenvm1g  16449  wlkl1loop  16465  wlklenvclwlk  16480  umgrclwwlkge2  16509  clwwlknp  16524  bj-charfun  16689  bj-findis  16861