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  614  mpjaodan  800  mpd3an3  1351  eueq2dc  2950  csbiegf  3141  difsnb  3781  reusv3i  4513  fimadmfo  5518  fvmpt3  5670  ffvelcdmd  5728  fnressn  5782  fliftel1  5875  f1oiso2  5908  riota5f  5936  1stvalg  6240  2ndvalg  6241  brtpos2  6349  tfrlemibxssdm  6425  dom2lem  6875  php5  6969  nnfi  6983  xpfi  7043  supisoti  7126  ordiso2  7151  omp1eomlem  7210  nnnninfeq2  7245  onenon  7305  oncardval  7307  cardonle  7308  recidnq  7521  archnqq  7545  prarloclemarch2  7547  recexprlem1ssl  7761  recexprlem1ssu  7762  recexprlemss1l  7763  recexprlemss1u  7764  recexprlemex  7765  0idsr  7895  lep1  8933  suprlubex  9040  uz11  9686  xnegid  9996  eluzfz2  10169  fzsuc  10206  fzsuc2  10216  fzp1disj  10217  fzneuz  10238  fzp1nel  10241  exbtwnzlemex  10409  flhalf  10462  modqval  10486  frec2uzsucd  10563  frecuzrdgsuc  10576  uzsinds  10606  seq3p1  10627  seqp1cd  10632  expubnd  10758  iexpcyc  10806  binom2sub1  10816  hashennn  10942  lswwrd  11057  eqs1  11100  pfxid  11157  wrdind  11193  wrd2ind  11194  shftfval  11202  shftcan1  11215  cjval  11226  reval  11230  imval  11231  cjmulrcl  11268  addcj  11272  absval  11382  resqrexlemdecn  11393  resqrexlemnmsq  11398  resqrexlemnm  11399  absneg  11431  abscj  11433  sqabsadd  11436  sqabssub  11437  ltabs  11468  dfabsmax  11598  negfi  11609  fsum3  11768  trirecip  11882  fprodseq  11964  efval  12042  ege2le3  12052  efcan  12057  sinval  12083  cosval  12084  efi4p  12098  resin4p  12099  recos4p  12100  sincossq  12129  eirraplem  12158  iddvds  12185  1dvds  12186  bezoutlemstep  12388  coprmgcdb  12480  1idssfct  12507  exprmfct  12530  oddpwdclemdc  12565  phival  12605  odzphi  12639  oddprmdvds  12747  setsn0fun  12939  gsumfzval  13293  0subm  13386  gsumfzz  13397  grprcan  13439  isgrpid2  13442  grpinvid  13462  mulgval  13528  mulgnn0z  13555  0subg  13605  qus0  13641  ghmker  13676  imasabl  13742  mgpplusgg  13756  mgpbasg  13758  mgpscag  13759  mgptsetg  13760  mgpdsg  13762  srgen1zr  13820  opprmulfvalg  13902  opprsllem  13906  1unit  13939  1rinv  13960  subrngmcl  14041  subrg1  14063  subrgmcl  14065  subrgdvds  14067  subrguss  14068  subrginv  14069  subrgdv  14070  subrgunit  14071  subrgugrp  14072  rnrhmsubrg  14084  lmodfopne  14158  lsssn0  14202  lspsn0  14254  lsp0  14255  sralmod  14282  2idlval  14334  cnfldneg  14405  zrhval  14449  cldval  14641  ntrfval  14642  clsfval  14643  neifval  14682  tx1cn  14811  ismet  14886  isxmet  14887  divcnap  15107  dvaddxxbr  15243  dvmulxxbr  15244  dvcoapbr  15249  sgmnncl  15530  1lgs  15590  lgs1  15591  bj-charfun  15877  bj-findis  16049