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  biadanid  614  mpjaodan  799  mpd3an3  1349  eueq2dc  2934  csbiegf  3125  difsnb  3762  reusv3i  4491  fimadmfo  5486  fvmpt3  5637  ffvelcdmd  5695  fnressn  5745  fliftel1  5838  f1oiso2  5871  riota5f  5899  1stvalg  6197  2ndvalg  6198  brtpos2  6306  tfrlemibxssdm  6382  dom2lem  6828  php5  6916  nnfi  6930  xpfi  6988  supisoti  7071  ordiso2  7096  omp1eomlem  7155  nnnninfeq2  7190  onenon  7246  oncardval  7248  cardonle  7249  recidnq  7455  archnqq  7479  prarloclemarch2  7481  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  recexprlemex  7699  0idsr  7829  lep1  8866  suprlubex  8973  uz11  9618  xnegid  9928  eluzfz2  10101  fzsuc  10138  fzsuc2  10148  fzp1disj  10149  fzneuz  10170  fzp1nel  10173  exbtwnzlemex  10321  flhalf  10374  modqval  10398  frec2uzsucd  10475  frecuzrdgsuc  10488  uzsinds  10518  seq3p1  10539  seqp1cd  10544  expubnd  10670  iexpcyc  10718  binom2sub1  10728  hashennn  10854  shftfval  10968  shftcan1  10981  cjval  10992  reval  10996  imval  10997  cjmulrcl  11034  addcj  11038  absval  11148  resqrexlemdecn  11159  resqrexlemnmsq  11164  resqrexlemnm  11165  absneg  11197  abscj  11199  sqabsadd  11202  sqabssub  11203  ltabs  11234  dfabsmax  11364  negfi  11374  fsum3  11533  trirecip  11647  fprodseq  11729  efval  11807  ege2le3  11817  efcan  11822  sinval  11848  cosval  11849  efi4p  11863  resin4p  11864  recos4p  11865  sincossq  11894  eirraplem  11923  iddvds  11950  1dvds  11951  bezoutlemstep  12137  coprmgcdb  12229  1idssfct  12256  exprmfct  12279  oddpwdclemdc  12314  phival  12354  odzphi  12387  oddprmdvds  12495  setsn0fun  12658  gsumfzval  12977  0subm  13059  gsumfzz  13070  grprcan  13112  isgrpid2  13115  grpinvid  13135  mulgval  13195  mulgnn0z  13222  0subg  13272  qus0  13308  ghmker  13343  imasabl  13409  mgpplusgg  13423  mgpbasg  13425  mgpscag  13426  mgptsetg  13427  mgpdsg  13429  srgen1zr  13487  opprmulfvalg  13569  opprsllem  13573  1unit  13606  1rinv  13627  subrngmcl  13708  subrg1  13730  subrgmcl  13732  subrgdvds  13734  subrguss  13735  subrginv  13736  subrgdv  13737  subrgunit  13738  subrgugrp  13739  rnrhmsubrg  13751  lmodfopne  13825  lsssn0  13869  lspsn0  13921  lsp0  13922  sralmod  13949  2idlval  14001  cnfldneg  14072  zrhval  14116  cldval  14278  ntrfval  14279  clsfval  14280  neifval  14319  tx1cn  14448  ismet  14523  isxmet  14524  divcnap  14744  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  1lgs  15200  lgs1  15201  bj-charfun  15369  bj-findis  15541