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  1317  eueq2dc  2861  csbiegf  3048  difsnb  3671  reusv3i  4388  fvmpt3  5508  ffvelrnd  5564  fnressn  5614  fliftel1  5703  f1oiso2  5736  riota5f  5762  1stvalg  6048  2ndvalg  6049  brtpos2  6156  tfrlemibxssdm  6232  dom2lem  6674  php5  6760  nnfi  6774  xpfi  6826  supisoti  6905  ordiso2  6928  omp1eomlem  6987  onenon  7057  oncardval  7059  cardonle  7060  recidnq  7225  archnqq  7249  prarloclemarch2  7251  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  recexprlemex  7469  0idsr  7599  lep1  8627  suprlubex  8734  uz11  9372  xnegid  9672  eluzfz2  9843  fzsuc  9880  fzsuc2  9890  fzp1disj  9891  fzneuz  9912  fzp1nel  9915  exbtwnzlemex  10058  flhalf  10106  modqval  10128  frec2uzsucd  10205  frecuzrdgsuc  10218  uzsinds  10246  seq3p1  10266  seqp1cd  10270  expubnd  10381  iexpcyc  10428  binom2sub1  10437  hashennn  10558  shftfval  10625  shftcan1  10638  cjval  10649  reval  10653  imval  10654  cjmulrcl  10691  addcj  10695  absval  10805  resqrexlemdecn  10816  resqrexlemnmsq  10821  resqrexlemnm  10822  absneg  10854  abscj  10856  sqabsadd  10859  sqabssub  10860  ltabs  10891  dfabsmax  11021  negfi  11031  fsum3  11188  trirecip  11302  fprodseq  11384  efval  11404  ege2le3  11414  efcan  11419  sinval  11445  cosval  11446  efi4p  11460  resin4p  11461  recos4p  11462  sincossq  11491  eirraplem  11519  iddvds  11542  1dvds  11543  bezoutlemstep  11721  coprmgcdb  11805  1idssfct  11832  exprmfct  11854  oddpwdclemdc  11887  phival  11925  setsn0fun  12035  cldval  12307  ntrfval  12308  clsfval  12309  neifval  12348  tx1cn  12477  ismet  12552  isxmet  12553  divcnap  12763  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  bj-findis  13348