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  618  mpjaodan  806  mpd3an3  1375  eueq2dc  2980  csbiegf  3172  difsnb  3821  reusv3i  4562  fimadmfo  5577  fvmpt3  5734  ffvelcdmd  5791  fnressn  5848  fliftel1  5945  f1oiso2  5978  riota5f  6008  1stvalg  6314  2ndvalg  6315  brtpos2  6460  tfrlemibxssdm  6536  dom2lem  6988  php5  7087  nnfi  7102  xpfi  7167  supisoti  7252  ordiso2  7277  omp1eomlem  7336  nnnninfeq2  7371  onenon  7431  oncardval  7433  cardonle  7434  recidnq  7656  archnqq  7680  prarloclemarch2  7682  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  recexprlemex  7900  0idsr  8030  lep1  9068  suprlubex  9175  uz11  9822  xnegid  10137  eluzfz2  10310  fzsuc  10347  fzsuc2  10357  fzp1disj  10358  fzneuz  10379  fzp1nel  10382  nn0p1elfzo  10465  exbtwnzlemex  10553  flhalf  10606  modqval  10630  frec2uzsucd  10707  frecuzrdgsuc  10720  uzsinds  10750  seq3p1  10771  seqp1cd  10776  expubnd  10902  iexpcyc  10950  binom2sub1  10960  hashennn  11086  lswwrd  11207  eqs1  11252  pfxid  11314  wrdind  11350  wrd2ind  11351  pfxccatpfx2  11365  swrdccat3blem  11367  shftfval  11442  shftcan1  11455  cjval  11466  reval  11470  imval  11471  cjmulrcl  11508  addcj  11512  absval  11622  resqrexlemdecn  11633  resqrexlemnmsq  11638  resqrexlemnm  11639  absneg  11671  abscj  11673  sqabsadd  11676  sqabssub  11677  ltabs  11708  dfabsmax  11838  negfi  11849  fsum3  12009  trirecip  12123  fprodseq  12205  efval  12283  ege2le3  12293  efcan  12298  sinval  12324  cosval  12325  efi4p  12339  resin4p  12340  recos4p  12341  sincossq  12370  eirraplem  12399  iddvds  12426  1dvds  12427  bezoutlemstep  12629  coprmgcdb  12721  1idssfct  12748  exprmfct  12771  oddpwdclemdc  12806  phival  12846  odzphi  12880  oddprmdvds  12988  setsn0fun  13180  gsumfzval  13535  0subm  13628  gsumfzz  13639  grprcan  13681  isgrpid2  13684  grpinvid  13704  mulgval  13770  mulgnn0z  13797  0subg  13847  qus0  13883  ghmker  13918  imasabl  13984  mgpplusgg  13999  mgpbasg  14001  mgpscag  14002  mgptsetg  14003  mgpdsg  14005  srgen1zr  14063  opprmulfvalg  14145  opprsllem  14149  1unit  14183  1rinv  14204  subrngmcl  14285  subrg1  14307  subrgmcl  14309  subrgdvds  14311  subrguss  14312  subrginv  14313  subrgdv  14314  subrgunit  14315  subrgugrp  14316  rnrhmsubrg  14328  lmodfopne  14402  lsssn0  14446  lspsn0  14498  lsp0  14499  sralmod  14526  2idlval  14578  cnfldneg  14649  zrhval  14693  cldval  14890  ntrfval  14891  clsfval  14892  neifval  14931  tx1cn  15060  ismet  15135  isxmet  15136  divcnap  15356  dvaddxxbr  15492  dvmulxxbr  15493  dvcoapbr  15498  sgmnncl  15782  1lgs  15842  lgs1  15843  uhgredgiedgb  16055  uhgriedg0edg0  16056  subgrprop3  16183  wlklenvm1  16262  wlklenvm1g  16263  wlkl1loop  16279  wlklenvclwlk  16294  umgrclwwlkge2  16323  clwwlknp  16338  bj-charfun  16503  bj-findis  16675