Theorem mpdan 417

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 408	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  419  mpan2  421  mpjaodan  787  mpd3an3  1316  eueq2dc  2852  csbiegf  3038  difsnb  3658  reusv3i  4375  fvmpt3  5493  ffvelrnd  5549  fnressn  5599  fliftel1  5688  f1oiso2  5721  riota5f  5747  1stvalg  6033  2ndvalg  6034  brtpos2  6141  tfrlemibxssdm  6217  dom2lem  6659  php5  6745  nnfi  6759  xpfi  6811  supisoti  6890  ordiso2  6913  omp1eomlem  6972  onenon  7033  oncardval  7035  cardonle  7036  recidnq  7194  archnqq  7218  prarloclemarch2  7220  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1l  7436  recexprlemss1u  7437  recexprlemex  7438  0idsr  7568  lep1  8596  suprlubex  8703  uz11  9341  xnegid  9635  eluzfz2  9805  fzsuc  9842  fzsuc2  9852  fzp1disj  9853  fzneuz  9874  fzp1nel  9877  exbtwnzlemex  10020  flhalf  10068  modqval  10090  frec2uzsucd  10167  frecuzrdgsuc  10180  uzsinds  10208  seq3p1  10228  seqp1cd  10232  expubnd  10343  iexpcyc  10390  binom2sub1  10399  hashennn  10519  shftfval  10586  shftcan1  10599  cjval  10610  reval  10614  imval  10615  cjmulrcl  10652  addcj  10656  absval  10766  resqrexlemdecn  10777  resqrexlemnmsq  10782  resqrexlemnm  10783  absneg  10815  abscj  10817  sqabsadd  10820  sqabssub  10821  ltabs  10852  dfabsmax  10982  negfi  10992  fsum3  11149  trirecip  11263  efval  11356  ege2le3  11366  efcan  11371  sinval  11398  cosval  11399  efi4p  11413  resin4p  11414  recos4p  11415  sincossq  11444  eirraplem  11472  iddvds  11495  1dvds  11496  bezoutlemstep  11674  coprmgcdb  11758  1idssfct  11785  exprmfct  11807  oddpwdclemdc  11840  phival  11878  setsn0fun  11985  cldval  12257  ntrfval  12258  clsfval  12259  neifval  12298  tx1cn  12427  ismet  12502  isxmet  12503  divcnap  12713  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  bj-findis  13166