Theorem mpdan 413

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpidan  415  mpan2  417  mpjaodan  748  mpd3an3  1275  eueq2dc  2791  csbiegf  2974  difsnb  3588  reusv3i  4296  fvmpt3  5398  ffvelrnd  5451  fnressn  5499  fliftel1  5589  f1oiso2  5622  riota5f  5648  1stvalg  5929  2ndvalg  5930  brtpos2  6032  tfrlemibxssdm  6108  dom2lem  6545  php5  6630  nnfi  6644  xpfi  6696  supisoti  6761  ordiso2  6784  onenon  6875  oncardval  6877  cardonle  6878  recidnq  7015  archnqq  7039  prarloclemarch2  7041  recexprlem1ssl  7255  recexprlem1ssu  7256  recexprlemss1l  7257  recexprlemss1u  7258  recexprlemex  7259  0idsr  7376  lep1  8369  suprlubex  8476  uz11  9104  eluzfz2  9509  fzsuc  9546  fzsuc2  9556  fzp1disj  9557  fzneuz  9578  fzp1nel  9581  exbtwnzlemex  9724  flhalf  9772  modqval  9794  frec2uzsucd  9871  frecuzrdgsuc  9884  uzsinds  9911  iseqp1  9945  iseqp1t  9946  seq3p1  9947  expubnd  10075  iexpcyc  10122  binom2sub1  10131  hashennn  10251  shftfval  10318  shftcan1  10331  cjval  10342  reval  10346  imval  10347  cjmulrcl  10384  addcj  10388  absval  10497  resqrexlemdecn  10508  resqrexlemnmsq  10513  resqrexlemnm  10514  absneg  10546  abscj  10548  sqabsadd  10551  sqabssub  10552  ltabs  10583  dfabsmax  10713  negfi  10722  fisum  10841  trirecip  10958  efval  11014  ege2le3  11024  efcan  11029  sinval  11056  cosval  11057  efi4p  11071  resin4p  11072  recos4p  11073  sincossq  11102  eirraplem  11127  iddvds  11150  1dvds  11151  bezoutlemstep  11327  coprmgcdb  11411  1idssfct  11438  exprmfct  11460  oddpwdclemdc  11492  phival  11530  setsn0fun  11594  cldval  11862  ntrfval  11863  clsfval  11864  neifval  11903  bj-findis  12178