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  mpjaodan  798  mpd3an3  1338  eueq2dc  2910  csbiegf  3100  difsnb  3735  reusv3i  4459  fvmpt3  5595  ffvelcdmd  5652  fnressn  5702  fliftel1  5794  f1oiso2  5827  riota5f  5854  1stvalg  6142  2ndvalg  6143  brtpos2  6251  tfrlemibxssdm  6327  dom2lem  6771  php5  6857  nnfi  6871  xpfi  6928  supisoti  7008  ordiso2  7033  omp1eomlem  7092  nnnninfeq2  7126  onenon  7182  oncardval  7184  cardonle  7185  recidnq  7391  archnqq  7415  prarloclemarch2  7417  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1l  7633  recexprlemss1u  7634  recexprlemex  7635  0idsr  7765  lep1  8801  suprlubex  8908  uz11  9549  xnegid  9858  eluzfz2  10031  fzsuc  10068  fzsuc2  10078  fzp1disj  10079  fzneuz  10100  fzp1nel  10103  exbtwnzlemex  10249  flhalf  10301  modqval  10323  frec2uzsucd  10400  frecuzrdgsuc  10413  uzsinds  10441  seq3p1  10461  seqp1cd  10465  expubnd  10576  iexpcyc  10624  binom2sub1  10634  hashennn  10759  shftfval  10829  shftcan1  10842  cjval  10853  reval  10857  imval  10858  cjmulrcl  10895  addcj  10899  absval  11009  resqrexlemdecn  11020  resqrexlemnmsq  11025  resqrexlemnm  11026  absneg  11058  abscj  11060  sqabsadd  11063  sqabssub  11064  ltabs  11095  dfabsmax  11225  negfi  11235  fsum3  11394  trirecip  11508  fprodseq  11590  efval  11668  ege2le3  11678  efcan  11683  sinval  11709  cosval  11710  efi4p  11724  resin4p  11725  recos4p  11726  sincossq  11755  eirraplem  11783  iddvds  11810  1dvds  11811  bezoutlemstep  11997  coprmgcdb  12087  1idssfct  12114  exprmfct  12137  oddpwdclemdc  12172  phival  12212  odzphi  12245  oddprmdvds  12351  setsn0fun  12498  0subm  12870  grprcan  12909  isgrpid2  12912  grpinvid  12929  mulgval  12985  mulgnn0z  13008  0subg  13057  mgpplusgg  13132  mgpbasg  13134  mgpscag  13135  mgptsetg  13136  mgpdsg  13138  srgen1zr  13169  opprmulfvalg  13240  opprsllem  13244  1unit  13274  1rinv  13295  subrg1  13350  subrgmcl  13352  subrgdvds  13354  subrguss  13355  subrginv  13356  subrgdv  13357  subrgunit  13358  subrgugrp  13359  cnfldneg  13437  cldval  13569  ntrfval  13570  clsfval  13571  neifval  13610  tx1cn  13739  ismet  13814  isxmet  13815  divcnap  14025  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  1lgs  14414  lgs1  14415  bj-charfun  14529  bj-findis  14701