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  2857  csbiegf  3043  difsnb  3663  reusv3i  4380  fvmpt3  5500  ffvelrnd  5556  fnressn  5606  fliftel1  5695  f1oiso2  5728  riota5f  5754  1stvalg  6040  2ndvalg  6041  brtpos2  6148  tfrlemibxssdm  6224  dom2lem  6666  php5  6752  nnfi  6766  xpfi  6818  supisoti  6897  ordiso2  6920  omp1eomlem  6979  onenon  7040  oncardval  7042  cardonle  7043  recidnq  7201  archnqq  7225  prarloclemarch2  7227  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  recexprlemex  7445  0idsr  7575  lep1  8603  suprlubex  8710  uz11  9348  xnegid  9642  eluzfz2  9812  fzsuc  9849  fzsuc2  9859  fzp1disj  9860  fzneuz  9881  fzp1nel  9884  exbtwnzlemex  10027  flhalf  10075  modqval  10097  frec2uzsucd  10174  frecuzrdgsuc  10187  uzsinds  10215  seq3p1  10235  seqp1cd  10239  expubnd  10350  iexpcyc  10397  binom2sub1  10406  hashennn  10526  shftfval  10593  shftcan1  10606  cjval  10617  reval  10621  imval  10622  cjmulrcl  10659  addcj  10663  absval  10773  resqrexlemdecn  10784  resqrexlemnmsq  10789  resqrexlemnm  10790  absneg  10822  abscj  10824  sqabsadd  10827  sqabssub  10828  ltabs  10859  dfabsmax  10989  negfi  10999  fsum3  11156  trirecip  11270  efval  11367  ege2le3  11377  efcan  11382  sinval  11409  cosval  11410  efi4p  11424  resin4p  11425  recos4p  11426  sincossq  11455  eirraplem  11483  iddvds  11506  1dvds  11507  bezoutlemstep  11685  coprmgcdb  11769  1idssfct  11796  exprmfct  11818  oddpwdclemdc  11851  phival  11889  setsn0fun  11996  cldval  12268  ntrfval  12269  clsfval  12270  neifval  12309  tx1cn  12438  ismet  12513  isxmet  12514  divcnap  12724  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  bj-findis  13177