Theorem mpdan 418

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  420  mpan2  422  mpjaodan  788  mpd3an3  1328  eueq2dc  2898  csbiegf  3087  difsnb  3715  reusv3i  4436  fvmpt3  5564  ffvelrnd  5620  fnressn  5670  fliftel1  5761  f1oiso2  5794  riota5f  5821  1stvalg  6107  2ndvalg  6108  brtpos2  6215  tfrlemibxssdm  6291  dom2lem  6734  php5  6820  nnfi  6834  xpfi  6891  supisoti  6971  ordiso2  6996  omp1eomlem  7055  nnnninfeq2  7089  onenon  7136  oncardval  7138  cardonle  7139  recidnq  7330  archnqq  7354  prarloclemarch2  7356  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1l  7572  recexprlemss1u  7573  recexprlemex  7574  0idsr  7704  lep1  8736  suprlubex  8843  uz11  9484  xnegid  9791  eluzfz2  9963  fzsuc  10000  fzsuc2  10010  fzp1disj  10011  fzneuz  10032  fzp1nel  10035  exbtwnzlemex  10181  flhalf  10233  modqval  10255  frec2uzsucd  10332  frecuzrdgsuc  10345  uzsinds  10373  seq3p1  10393  seqp1cd  10397  expubnd  10508  iexpcyc  10555  binom2sub1  10565  hashennn  10689  shftfval  10759  shftcan1  10772  cjval  10783  reval  10787  imval  10788  cjmulrcl  10825  addcj  10829  absval  10939  resqrexlemdecn  10950  resqrexlemnmsq  10955  resqrexlemnm  10956  absneg  10988  abscj  10990  sqabsadd  10993  sqabssub  10994  ltabs  11025  dfabsmax  11155  negfi  11165  fsum3  11324  trirecip  11438  fprodseq  11520  efval  11598  ege2le3  11608  efcan  11613  sinval  11639  cosval  11640  efi4p  11654  resin4p  11655  recos4p  11656  sincossq  11685  eirraplem  11713  iddvds  11740  1dvds  11741  bezoutlemstep  11926  coprmgcdb  12016  1idssfct  12043  exprmfct  12066  oddpwdclemdc  12101  phival  12141  odzphi  12174  oddprmdvds  12280  setsn0fun  12427  cldval  12699  ntrfval  12700  clsfval  12701  neifval  12740  tx1cn  12869  ismet  12944  isxmet  12945  divcnap  13155  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  1lgs  13544  lgs1  13545  bj-charfun  13649  bj-findis  13821