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  2993  csbiegf  3185  difsnb  3842  reusv3i  4585  fimadmfo  5604  fvmpt3  5761  ffvelcdmd  5818  fnressn  5875  fliftel1  5973  f1oiso2  6006  riota5f  6038  1stvalg  6349  2ndvalg  6350  brtpos2  6495  tfrlemibxssdm  6571  dom2lem  7024  php5  7125  nnfi  7140  xpfi  7205  supisoti  7314  ordiso2  7339  omp1eomlem  7398  nnnninfeq2  7433  onenon  7493  oncardval  7495  cardonle  7496  recidnq  7724  archnqq  7748  prarloclemarch2  7750  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  recexprlemex  7968  0idsr  8098  lep1  9139  suprlubex  9246  uz11  9898  xnegid  10214  eluzfz2  10389  fzsuc  10427  fzsuc2  10438  fzp1disj  10439  fzneuz  10460  fzp1nel  10463  nn0p1elfzo  10546  exbtwnzlemex  10636  flhalf  10689  modqval  10713  frec2uzsucd  10790  frecuzrdgsuc  10803  uzsinds  10833  seq3p1  10854  seqp1cd  10859  expubnd  10985  iexpcyc  11033  binom2sub1  11043  hashennn  11171  lswwrd  11299  eqs1  11344  pfxid  11406  wrdind  11442  wrd2ind  11443  pfxccatpfx2  11457  swrdccat3blem  11459  shftfval  11534  shftcan1  11547  cjval  11558  reval  11562  imval  11563  cjmulrcl  11600  addcj  11604  absval  11715  resqrexlemdecn  11726  resqrexlemnmsq  11731  resqrexlemnm  11732  absneg  11764  abscj  11766  sqabsadd  11769  sqabssub  11770  ltabs  11801  dfabsmax  11931  negfi  11942  fsum3  12102  trirecip  12216  fprodseq  12298  efval  12376  ege2le3  12386  efcan  12391  sinval  12417  cosval  12418  efi4p  12432  resin4p  12433  recos4p  12434  sincossq  12463  eirraplem  12492  iddvds  12519  1dvds  12520  bezoutlemstep  12722  coprmgcdb  12814  1idssfct  12841  exprmfct  12864  oddpwdclemdc  12899  phival  12939  odzphi  12973  oddprmdvds  13081  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemsi  13206  ballotfilemfrci  13219  setsn0fun  13337  gsumfzval  13658  0subm  13743  gsumfzz  13754  grprcan  13796  isgrpid2  13799  grpinvid  13819  mulgval  13879  mulgnn0z  13906  0subg  13956  qus0  13992  ghmker  14027  imasabl  14093  mgpplusgg  14167  mgpbasg  14169  mgpscag  14170  mgptsetg  14171  mgpdsg  14173  rngen1zr0  14205  srgen1zr0  14235  opprmulfvalg  14317  opprsllem  14321  1unit  14356  1rinv  14377  subrngmcl  14459  subrg1  14481  subrgmcl  14483  subrgdvds  14485  subrguss  14486  subrginv  14487  subrgdv  14488  subrgunit  14489  subrgugrp  14490  rnrhmsubrg  14502  lmodfopne  14604  lsssn0  14648  lspsn0  14700  lsp0  14701  sralmod  14728  2idlval  14780  cnfldneg  14851  zrhval  14895  psrbagfsupp  14949  cldval  15094  ntrfval  15095  clsfval  15096  neifval  15135  tx1cn  15264  ismet  15339  isxmet  15340  divcnap  15560  dvaddxxbr  15696  dvmulxxbr  15697  dvcoapbr  15702  sgmnncl  15986  1lgs  16046  lgs1  16047  uhgredgiedgb  16259  uhgriedg0edg0  16260  subgrprop3  16387  wlklenvm1  16466  wlklenvm1g  16467  wlkl1loop  16483  wlklenvclwlk  16498  umgrclwwlkge2  16527  clwwlknp  16542  bj-charfun  16717  bj-findis  16889