Theorem mpdan 419

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 409	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpidan  421  mpan2  423  mpjaodan  793  mpd3an3  1333  eueq2dc  2903  csbiegf  3092  difsnb  3723  reusv3i  4444  fvmpt3  5575  ffvelrnd  5632  fnressn  5682  fliftel1  5773  f1oiso2  5806  riota5f  5833  1stvalg  6121  2ndvalg  6122  brtpos2  6230  tfrlemibxssdm  6306  dom2lem  6750  php5  6836  nnfi  6850  xpfi  6907  supisoti  6987  ordiso2  7012  omp1eomlem  7071  nnnninfeq2  7105  onenon  7161  oncardval  7163  cardonle  7164  recidnq  7355  archnqq  7379  prarloclemarch2  7381  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  recexprlemex  7599  0idsr  7729  lep1  8761  suprlubex  8868  uz11  9509  xnegid  9816  eluzfz2  9988  fzsuc  10025  fzsuc2  10035  fzp1disj  10036  fzneuz  10057  fzp1nel  10060  exbtwnzlemex  10206  flhalf  10258  modqval  10280  frec2uzsucd  10357  frecuzrdgsuc  10370  uzsinds  10398  seq3p1  10418  seqp1cd  10422  expubnd  10533  iexpcyc  10580  binom2sub1  10590  hashennn  10714  shftfval  10785  shftcan1  10798  cjval  10809  reval  10813  imval  10814  cjmulrcl  10851  addcj  10855  absval  10965  resqrexlemdecn  10976  resqrexlemnmsq  10981  resqrexlemnm  10982  absneg  11014  abscj  11016  sqabsadd  11019  sqabssub  11020  ltabs  11051  dfabsmax  11181  negfi  11191  fsum3  11350  trirecip  11464  fprodseq  11546  efval  11624  ege2le3  11634  efcan  11639  sinval  11665  cosval  11666  efi4p  11680  resin4p  11681  recos4p  11682  sincossq  11711  eirraplem  11739  iddvds  11766  1dvds  11767  bezoutlemstep  11952  coprmgcdb  12042  1idssfct  12069  exprmfct  12092  oddpwdclemdc  12127  phival  12167  odzphi  12200  oddprmdvds  12306  setsn0fun  12453  0subm  12702  grprcan  12740  isgrpid2  12743  grpinvid  12760  cldval  12893  ntrfval  12894  clsfval  12895  neifval  12934  tx1cn  13063  ismet  13138  isxmet  13139  divcnap  13349  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  1lgs  13738  lgs1  13739  bj-charfun  13842  bj-findis  14014