Theorem mpdan 412

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mpan2  415  mpjaodan  744  mpd3an3  1269  eueq2dc  2765  csbiegf  2946  difsnb  3528  reusv3i  4209  fvmpt3  5272  ffvelrnd  5324  fnressn  5370  fliftel1  5454  f1oiso2  5486  riota5f  5512  1stvalg  5789  2ndvalg  5790  brtpos2  5889  tfrlemibxssdm  5964  dom2lem  6275  php5  6344  nnfi  6357  supisoti  6423  ordiso2  6446  onenon  6453  oncardval  6455  cardonle  6456  recidnq  6583  archnqq  6607  prarloclemarch2  6609  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  recexprlemex  6827  0idsr  6944  lep1  7923  suprlubex  8030  uz11  8641  eluzfz2  9051  fzsuc  9086  fzsuc2  9096  fzp1disj  9097  fzneuz  9118  fzp1nel  9121  flhalf  9304  modqval  9326  frecuzrdgsuc  9417  uzsinds  9428  iseqcl  9443  iseqp1  9445  expubnd  9533  iexpcyc  9579  shftfval  9709  shftcan1  9722  cjval  9732  reval  9736  imval  9737  cjmulrcl  9774  addcj  9778  absval  9887  resqrexlemdecn  9898  resqrexlemnmsq  9903  resqrexlemnm  9904  absneg  9936  abscj  9938  sqabsadd  9941  sqabssub  9942  ltabs  9973  dfabsmax  10103  negfi  10110  iddvds  10208  1dvds  10209  bezoutlemstep  10386  coprmgcdb  10470  1idssfct  10497  exprmfct  10519  oddpwdclemdc  10551  bj-findis  10774