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  2937  csbiegf  3128  difsnb  3765  reusv3i  4494  fimadmfo  5489  fvmpt3  5640  ffvelcdmd  5698  fnressn  5748  fliftel1  5841  f1oiso2  5874  riota5f  5902  1stvalg  6200  2ndvalg  6201  brtpos2  6309  tfrlemibxssdm  6385  dom2lem  6831  php5  6919  nnfi  6933  xpfi  6993  supisoti  7076  ordiso2  7101  omp1eomlem  7160  nnnninfeq2  7195  onenon  7251  oncardval  7253  cardonle  7254  recidnq  7460  archnqq  7484  prarloclemarch2  7486  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  recexprlemex  7704  0idsr  7834  lep1  8872  suprlubex  8979  uz11  9624  xnegid  9934  eluzfz2  10107  fzsuc  10144  fzsuc2  10154  fzp1disj  10155  fzneuz  10176  fzp1nel  10179  exbtwnzlemex  10339  flhalf  10392  modqval  10416  frec2uzsucd  10493  frecuzrdgsuc  10506  uzsinds  10536  seq3p1  10557  seqp1cd  10562  expubnd  10688  iexpcyc  10736  binom2sub1  10746  hashennn  10872  shftfval  10986  shftcan1  10999  cjval  11010  reval  11014  imval  11015  cjmulrcl  11052  addcj  11056  absval  11166  resqrexlemdecn  11177  resqrexlemnmsq  11182  resqrexlemnm  11183  absneg  11215  abscj  11217  sqabsadd  11220  sqabssub  11221  ltabs  11252  dfabsmax  11382  negfi  11393  fsum3  11552  trirecip  11666  fprodseq  11748  efval  11826  ege2le3  11836  efcan  11841  sinval  11867  cosval  11868  efi4p  11882  resin4p  11883  recos4p  11884  sincossq  11913  eirraplem  11942  iddvds  11969  1dvds  11970  bezoutlemstep  12164  coprmgcdb  12256  1idssfct  12283  exprmfct  12306  oddpwdclemdc  12341  phival  12381  odzphi  12415  oddprmdvds  12523  setsn0fun  12715  gsumfzval  13034  0subm  13116  gsumfzz  13127  grprcan  13169  isgrpid2  13172  grpinvid  13192  mulgval  13252  mulgnn0z  13279  0subg  13329  qus0  13365  ghmker  13400  imasabl  13466  mgpplusgg  13480  mgpbasg  13482  mgpscag  13483  mgptsetg  13484  mgpdsg  13486  srgen1zr  13544  opprmulfvalg  13626  opprsllem  13630  1unit  13663  1rinv  13684  subrngmcl  13765  subrg1  13787  subrgmcl  13789  subrgdvds  13791  subrguss  13792  subrginv  13793  subrgdv  13794  subrgunit  13795  subrgugrp  13796  rnrhmsubrg  13808  lmodfopne  13882  lsssn0  13926  lspsn0  13978  lsp0  13979  sralmod  14006  2idlval  14058  cnfldneg  14129  zrhval  14173  cldval  14335  ntrfval  14336  clsfval  14337  neifval  14376  tx1cn  14505  ismet  14580  isxmet  14581  divcnap  14801  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  sgmnncl  15224  1lgs  15284  lgs1  15285  bj-charfun  15453  bj-findis  15625