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  2989  csbiegf  3181  difsnb  3836  reusv3i  4579  fimadmfo  5598  fvmpt3  5755  ffvelcdmd  5812  fnressn  5869  fliftel1  5966  f1oiso2  5999  riota5f  6029  1stvalg  6335  2ndvalg  6336  brtpos2  6481  tfrlemibxssdm  6557  dom2lem  7010  php5  7111  nnfi  7126  xpfi  7191  supisoti  7300  ordiso2  7325  omp1eomlem  7384  nnnninfeq2  7419  onenon  7479  oncardval  7481  cardonle  7482  recidnq  7707  archnqq  7731  prarloclemarch2  7733  recexprlem1ssl  7947  recexprlem1ssu  7948  recexprlemss1l  7949  recexprlemss1u  7950  recexprlemex  7951  0idsr  8081  lep1  9118  suprlubex  9225  uz11  9876  xnegid  10191  eluzfz2  10365  fzsuc  10402  fzsuc2  10412  fzp1disj  10413  fzneuz  10434  fzp1nel  10437  nn0p1elfzo  10520  exbtwnzlemex  10608  flhalf  10661  modqval  10685  frec2uzsucd  10762  frecuzrdgsuc  10775  uzsinds  10805  seq3p1  10826  seqp1cd  10831  expubnd  10957  iexpcyc  11005  binom2sub1  11015  hashennn  11141  lswwrd  11267  eqs1  11312  pfxid  11374  wrdind  11410  wrd2ind  11411  pfxccatpfx2  11425  swrdccat3blem  11427  shftfval  11502  shftcan1  11515  cjval  11526  reval  11530  imval  11531  cjmulrcl  11568  addcj  11572  absval  11682  resqrexlemdecn  11693  resqrexlemnmsq  11698  resqrexlemnm  11699  absneg  11731  abscj  11733  sqabsadd  11736  sqabssub  11737  ltabs  11768  dfabsmax  11898  negfi  11909  fsum3  12069  trirecip  12183  fprodseq  12265  efval  12343  ege2le3  12353  efcan  12358  sinval  12384  cosval  12385  efi4p  12399  resin4p  12400  recos4p  12401  sincossq  12430  eirraplem  12459  iddvds  12486  1dvds  12487  bezoutlemstep  12689  coprmgcdb  12781  1idssfct  12808  exprmfct  12831  oddpwdclemdc  12866  phival  12906  odzphi  12940  oddprmdvds  13048  setsn0fun  13241  gsumfzval  13596  0subm  13689  gsumfzz  13700  grprcan  13742  isgrpid2  13745  grpinvid  13765  mulgval  13831  mulgnn0z  13858  0subg  13908  qus0  13944  ghmker  13979  imasabl  14045  mgpplusgg  14060  mgpbasg  14062  mgpscag  14063  mgptsetg  14064  mgpdsg  14066  srgen1zr  14124  opprmulfvalg  14206  opprsllem  14210  1unit  14244  1rinv  14265  subrngmcl  14346  subrg1  14368  subrgmcl  14370  subrgdvds  14372  subrguss  14373  subrginv  14374  subrgdv  14375  subrgunit  14376  subrgugrp  14377  rnrhmsubrg  14389  lmodfopne  14466  lsssn0  14510  lspsn0  14562  lsp0  14563  sralmod  14590  2idlval  14642  cnfldneg  14713  zrhval  14757  psrbagfsupp  14811  cldval  14956  ntrfval  14957  clsfval  14958  neifval  14997  tx1cn  15126  ismet  15201  isxmet  15202  divcnap  15422  dvaddxxbr  15558  dvmulxxbr  15559  dvcoapbr  15564  sgmnncl  15848  1lgs  15908  lgs1  15909  uhgredgiedgb  16121  uhgriedg0edg0  16122  subgrprop3  16249  wlklenvm1  16328  wlklenvm1g  16329  wlkl1loop  16345  wlklenvclwlk  16360  umgrclwwlkge2  16389  clwwlknp  16404  bj-charfun  16569  bj-findis  16741