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  1320  eueq2dc  2885  csbiegf  3074  difsnb  3699  reusv3i  4418  fvmpt3  5546  ffvelrnd  5602  fnressn  5652  fliftel1  5741  f1oiso2  5774  riota5f  5801  1stvalg  6087  2ndvalg  6088  brtpos2  6195  tfrlemibxssdm  6271  dom2lem  6714  php5  6800  nnfi  6814  xpfi  6871  supisoti  6950  ordiso2  6973  omp1eomlem  7032  nnnninfeq2  7066  onenon  7113  oncardval  7115  cardonle  7116  recidnq  7307  archnqq  7331  prarloclemarch2  7333  recexprlem1ssl  7547  recexprlem1ssu  7548  recexprlemss1l  7549  recexprlemss1u  7550  recexprlemex  7551  0idsr  7681  lep1  8710  suprlubex  8817  uz11  9455  xnegid  9756  eluzfz2  9927  fzsuc  9964  fzsuc2  9974  fzp1disj  9975  fzneuz  9996  fzp1nel  9999  exbtwnzlemex  10142  flhalf  10194  modqval  10216  frec2uzsucd  10293  frecuzrdgsuc  10306  uzsinds  10334  seq3p1  10354  seqp1cd  10358  expubnd  10469  iexpcyc  10516  binom2sub1  10525  hashennn  10647  shftfval  10714  shftcan1  10727  cjval  10738  reval  10742  imval  10743  cjmulrcl  10780  addcj  10784  absval  10894  resqrexlemdecn  10905  resqrexlemnmsq  10910  resqrexlemnm  10911  absneg  10943  abscj  10945  sqabsadd  10948  sqabssub  10949  ltabs  10980  dfabsmax  11110  negfi  11120  fsum3  11277  trirecip  11391  fprodseq  11473  efval  11551  ege2le3  11561  efcan  11566  sinval  11592  cosval  11593  efi4p  11607  resin4p  11608  recos4p  11609  sincossq  11638  eirraplem  11666  iddvds  11692  1dvds  11693  bezoutlemstep  11872  coprmgcdb  11956  1idssfct  11983  exprmfct  12005  oddpwdclemdc  12038  phival  12076  setsn0fun  12198  cldval  12470  ntrfval  12471  clsfval  12472  neifval  12511  tx1cn  12640  ismet  12715  isxmet  12716  divcnap  12926  dvaddxxbr  13036  dvmulxxbr  13037  dvcoapbr  13042  bj-charfun  13353  bj-findis  13525