Theorem mpdan 421

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpidan  423  mpan2  425  mpjaodan  798  mpd3an3  1338  eueq2dc  2910  csbiegf  3100  difsnb  3735  reusv3i  4457  fvmpt3  5592  ffvelcdmd  5649  fnressn  5699  fliftel1  5790  f1oiso2  5823  riota5f  5850  1stvalg  6138  2ndvalg  6139  brtpos2  6247  tfrlemibxssdm  6323  dom2lem  6767  php5  6853  nnfi  6867  xpfi  6924  supisoti  7004  ordiso2  7029  omp1eomlem  7088  nnnninfeq2  7122  onenon  7178  oncardval  7180  cardonle  7181  recidnq  7387  archnqq  7411  prarloclemarch2  7413  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1l  7629  recexprlemss1u  7630  recexprlemex  7631  0idsr  7761  lep1  8796  suprlubex  8903  uz11  9544  xnegid  9853  eluzfz2  10025  fzsuc  10062  fzsuc2  10072  fzp1disj  10073  fzneuz  10094  fzp1nel  10097  exbtwnzlemex  10243  flhalf  10295  modqval  10317  frec2uzsucd  10394  frecuzrdgsuc  10407  uzsinds  10435  seq3p1  10455  seqp1cd  10459  expubnd  10570  iexpcyc  10617  binom2sub1  10627  hashennn  10751  shftfval  10821  shftcan1  10834  cjval  10845  reval  10849  imval  10850  cjmulrcl  10887  addcj  10891  absval  11001  resqrexlemdecn  11012  resqrexlemnmsq  11017  resqrexlemnm  11018  absneg  11050  abscj  11052  sqabsadd  11055  sqabssub  11056  ltabs  11087  dfabsmax  11217  negfi  11227  fsum3  11386  trirecip  11500  fprodseq  11582  efval  11660  ege2le3  11670  efcan  11675  sinval  11701  cosval  11702  efi4p  11716  resin4p  11717  recos4p  11718  sincossq  11747  eirraplem  11775  iddvds  11802  1dvds  11803  bezoutlemstep  11988  coprmgcdb  12078  1idssfct  12105  exprmfct  12128  oddpwdclemdc  12163  phival  12203  odzphi  12236  oddprmdvds  12342  setsn0fun  12489  0subm  12799  grprcan  12838  isgrpid2  12841  grpinvid  12858  mulgval  12914  mulgnn0z  12937  0subg  12985  mgpplusgg  13034  mgpbasg  13036  mgpscag  13037  mgptsetg  13038  mgpdsg  13040  srgen1zr  13071  opprmulfvalg  13141  opprsllem  13145  1unit  13175  1rinv  13196  cnfldneg  13272  cldval  13381  ntrfval  13382  clsfval  13383  neifval  13422  tx1cn  13551  ismet  13626  isxmet  13627  divcnap  13837  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  1lgs  14226  lgs1  14227  bj-charfun  14330  bj-findis  14502