Theorem mpdan 425

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpidan  427  mpan2  429  biadanid  622  mpjaodan  810  mpd3an3  1379  eueq2dc  2999  csbiegf  3191  difsnb  3858  reusv3i  4607  fimadmfo  5627  fvmpt3  5787  ffvelcdmd  5847  fnressn  5904  fliftel1  6003  f1oiso2  6036  riota5f  6068  1stvalg  6380  2ndvalg  6381  brtpos2  6527  tfrlemibxssdm  6603  dom2lem  7064  php5  7165  nnfi  7180  xpfi  7245  supisoti  7357  ordiso2  7382  omp1eomlem  7441  nnnninfeq2  7476  onenon  7536  oncardval  7538  cardonle  7539  recidnq  7767  archnqq  7791  prarloclemarch2  7793  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  recexprlemex  8011  0idsr  8141  lep1  9184  suprlubex  9291  uz11  9961  xnegid  10278  eluzfz2  10453  fzsuc  10492  fzsuc2  10503  fzp1disj  10504  fzneuz  10525  fzp1nel  10528  nn0p1elfzo  10611  exbtwnzlemex  10701  flhalf  10758  modqval  10782  frec2uzsucd  10859  frecuzrdgsuc  10872  uzsinds  10902  seq3p1  10923  seqp1cd  10928  expubnd  11054  iexpcyc  11102  binom2sub1  11112  hashennn  11241  lswwrd  11373  eqs1  11418  pfxid  11480  wrdind  11516  wrd2ind  11517  pfxccatpfx2  11531  swrdccat3blem  11533  shftfval  11608  shftcan1  11621  cjval  11632  reval  11636  imval  11637  cjmulrcl  11674  addcj  11678  absval  11789  resqrexlemdecn  11800  resqrexlemnmsq  11805  resqrexlemnm  11806  absneg  11838  abscj  11840  sqabsadd  11843  sqabssub  11844  ltabs  11876  dfabsmax  12006  negfi  12017  fsum3  12179  trirecip  12293  fprodseq  12375  efval  12453  ege2le3  12463  efcan  12468  sinval  12494  cosval  12495  efi4p  12509  resin4p  12510  recos4p  12511  sincossq  12540  eirraplem  12569  iddvds  12596  1dvds  12597  bezoutlemstep  12799  coprmgcdb  12891  1idssfct  12918  exprmfct  12942  pwbdvdslemn  12969  phival  13020  odzphi  13054  oddprmdvds  13162  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsi  13316  ballotfilemfrci  13329  setsn0fun  13447  gzsumfzval  13770  0subm  13850  grprcan  13901  isgrpid2  13904  grpinvid  13924  mulgval  13984  mulgnn0z  14011  0subg  14061  qus0  14097  ghmker  14132  imasabl  14230  mgpplusgg  14328  mgpbasg  14331  mgpscag  14333  mgptsetg  14334  mgpdsg  14336  rngen1zr0  14368  srgen1zr0  14399  opprmulfvalg  14484  opprsllem  14488  1unit  14523  1rinv  14544  subrngmcl  14626  subrg1  14648  subrgmcl  14650  subrgdvds  14652  subrguss  14653  subrginv  14654  subrgdv  14655  subrgunit  14656  subrgugrp  14657  rnrhmsubrg  14669  lmodfopne  14772  lsssn0  14816  lspsn0  14868  lsp0  14869  sralmod  14896  2idlval  14948  cnfldneg  15019  zrhval  15061  psrdifi  15222  psrdirfi  15223  cldval  15358  ntrfval  15359  clsfval  15360  neifval  15399  tx1cn  15528  ismet  15603  isxmet  15604  divcnap  15824  dvaddxxbr  15960  dvmulxxbr  15961  dvcoapbr  15966  sgmnncl  16290  1lgs  16400  lgs1  16401  uhgredgiedgb  16613  uhgriedg0edg0  16614  subgrprop3  16741  wlklenvm1  16820  wlklenvm1g  16821  wlkl1loop  16837  wlklenvclwlk  16852  umgrclwwlkge2  16881  clwwlknp  16896  bj-charfun  17071  bj-findis  17243