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  616  mpjaodan  803  mpd3an3  1372  eueq2dc  2976  csbiegf  3168  difsnb  3810  reusv3i  4547  fimadmfo  5553  fvmpt3  5706  ffvelcdmd  5764  fnressn  5818  fliftel1  5911  f1oiso2  5944  riota5f  5974  1stvalg  6278  2ndvalg  6279  brtpos2  6387  tfrlemibxssdm  6463  dom2lem  6913  php5  7007  nnfi  7022  xpfi  7082  supisoti  7165  ordiso2  7190  omp1eomlem  7249  nnnninfeq2  7284  onenon  7344  oncardval  7346  cardonle  7347  recidnq  7568  archnqq  7592  prarloclemarch2  7594  recexprlem1ssl  7808  recexprlem1ssu  7809  recexprlemss1l  7810  recexprlemss1u  7811  recexprlemex  7812  0idsr  7942  lep1  8980  suprlubex  9087  uz11  9733  xnegid  10043  eluzfz2  10216  fzsuc  10253  fzsuc2  10263  fzp1disj  10264  fzneuz  10285  fzp1nel  10288  exbtwnzlemex  10456  flhalf  10509  modqval  10533  frec2uzsucd  10610  frecuzrdgsuc  10623  uzsinds  10653  seq3p1  10674  seqp1cd  10679  expubnd  10805  iexpcyc  10853  binom2sub1  10863  hashennn  10989  lswwrd  11104  eqs1  11147  pfxid  11204  wrdind  11240  wrd2ind  11241  pfxccatpfx2  11255  swrdccat3blem  11257  shftfval  11318  shftcan1  11331  cjval  11342  reval  11346  imval  11347  cjmulrcl  11384  addcj  11388  absval  11498  resqrexlemdecn  11509  resqrexlemnmsq  11514  resqrexlemnm  11515  absneg  11547  abscj  11549  sqabsadd  11552  sqabssub  11553  ltabs  11584  dfabsmax  11714  negfi  11725  fsum3  11884  trirecip  11998  fprodseq  12080  efval  12158  ege2le3  12168  efcan  12173  sinval  12199  cosval  12200  efi4p  12214  resin4p  12215  recos4p  12216  sincossq  12245  eirraplem  12274  iddvds  12301  1dvds  12302  bezoutlemstep  12504  coprmgcdb  12596  1idssfct  12623  exprmfct  12646  oddpwdclemdc  12681  phival  12721  odzphi  12755  oddprmdvds  12863  setsn0fun  13055  gsumfzval  13410  0subm  13503  gsumfzz  13514  grprcan  13556  isgrpid2  13559  grpinvid  13579  mulgval  13645  mulgnn0z  13672  0subg  13722  qus0  13758  ghmker  13793  imasabl  13859  mgpplusgg  13873  mgpbasg  13875  mgpscag  13876  mgptsetg  13877  mgpdsg  13879  srgen1zr  13937  opprmulfvalg  14019  opprsllem  14023  1unit  14056  1rinv  14077  subrngmcl  14158  subrg1  14180  subrgmcl  14182  subrgdvds  14184  subrguss  14185  subrginv  14186  subrgdv  14187  subrgunit  14188  subrgugrp  14189  rnrhmsubrg  14201  lmodfopne  14275  lsssn0  14319  lspsn0  14371  lsp0  14372  sralmod  14399  2idlval  14451  cnfldneg  14522  zrhval  14566  cldval  14758  ntrfval  14759  clsfval  14760  neifval  14799  tx1cn  14928  ismet  15003  isxmet  15004  divcnap  15224  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366  sgmnncl  15647  1lgs  15707  lgs1  15708  uhgredgiedgb  15917  uhgriedg0edg0  15918  bj-charfun  16100  bj-findis  16272