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  4605  fimadmfo  5624  fvmpt3  5784  ffvelcdmd  5844  fnressn  5901  fliftel1  6000  f1oiso2  6033  riota5f  6065  1stvalg  6376  2ndvalg  6377  brtpos2  6522  tfrlemibxssdm  6598  dom2lem  7058  php5  7159  nnfi  7174  xpfi  7239  supisoti  7351  ordiso2  7376  omp1eomlem  7435  nnnninfeq2  7470  onenon  7530  oncardval  7532  cardonle  7533  recidnq  7761  archnqq  7785  prarloclemarch2  7787  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  recexprlemex  8005  0idsr  8135  lep1  9178  suprlubex  9285  uz11  9955  xnegid  10272  eluzfz2  10447  fzsuc  10486  fzsuc2  10497  fzp1disj  10498  fzneuz  10519  fzp1nel  10522  nn0p1elfzo  10605  exbtwnzlemex  10695  flhalf  10751  modqval  10775  frec2uzsucd  10852  frecuzrdgsuc  10865  uzsinds  10895  seq3p1  10916  seqp1cd  10921  expubnd  11047  iexpcyc  11095  binom2sub1  11105  hashennn  11234  lswwrd  11366  eqs1  11411  pfxid  11473  wrdind  11509  wrd2ind  11510  pfxccatpfx2  11524  swrdccat3blem  11526  shftfval  11601  shftcan1  11614  cjval  11625  reval  11629  imval  11630  cjmulrcl  11667  addcj  11671  absval  11782  resqrexlemdecn  11793  resqrexlemnmsq  11798  resqrexlemnm  11799  absneg  11831  abscj  11833  sqabsadd  11836  sqabssub  11837  ltabs  11869  dfabsmax  11999  negfi  12010  fsum3  12172  trirecip  12286  fprodseq  12368  efval  12446  ege2le3  12456  efcan  12461  sinval  12487  cosval  12488  efi4p  12502  resin4p  12503  recos4p  12504  sincossq  12533  eirraplem  12562  iddvds  12589  1dvds  12590  bezoutlemstep  12792  coprmgcdb  12884  1idssfct  12911  exprmfct  12935  pwbdvdslemn  12962  phival  13013  odzphi  13047  oddprmdvds  13155  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemsi  13309  ballotfilemfrci  13322  setsn0fun  13440  gzsumfzval  13762  0subm  13842  grprcan  13893  isgrpid2  13896  grpinvid  13916  mulgval  13976  mulgnn0z  14003  0subg  14053  qus0  14089  ghmker  14124  imasabl  14191  mgpplusgg  14272  mgpbasg  14275  mgpscag  14277  mgptsetg  14278  mgpdsg  14280  rngen1zr0  14312  srgen1zr0  14343  opprmulfvalg  14426  opprsllem  14430  1unit  14465  1rinv  14486  subrngmcl  14568  subrg1  14590  subrgmcl  14592  subrgdvds  14594  subrguss  14595  subrginv  14596  subrgdv  14597  subrgunit  14598  subrgugrp  14599  rnrhmsubrg  14611  lmodfopne  14714  lsssn0  14758  lspsn0  14810  lsp0  14811  sralmod  14838  2idlval  14890  cnfldneg  14961  zrhval  15003  psrbagfsupp  15106  cldval  15252  ntrfval  15253  clsfval  15254  neifval  15293  tx1cn  15422  ismet  15497  isxmet  15498  divcnap  15718  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  sgmnncl  16179  1lgs  16284  lgs1  16285  uhgredgiedgb  16497  uhgriedg0edg0  16498  subgrprop3  16625  wlklenvm1  16704  wlklenvm1g  16705  wlkl1loop  16721  wlklenvclwlk  16736  umgrclwwlkge2  16765  clwwlknp  16780  bj-charfun  16955  bj-findis  17127