Theorem simpr3 1005

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr3	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 999	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simplr3  1041  simprr3  1047  simp1r3  1095  simp2r3  1101  simp3r3  1107  3anandis  1347  isopolem  5825  tfrlemibacc  6329  tfrlemibxssdm  6330  tfrlemibfn  6331  tfr1onlembacc  6345  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfrcllembacc  6358  tfrcllembxssdm  6359  tfrcllembfn  6360  elfir  6974  prloc  7492  prmuloc2  7568  ltntri  8087  eluzuzle  9538  xlesubadd  9885  elioc2  9938  elico2  9939  elicc2  9940  fseq1p1m1  10096  seq3f1olemp  10504  seq3f1oleml  10505  bcval5  10745  hashdifpr  10802  isumss2  11403  tanaddap  11749  dvds2ln  11833  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  f1ovscpbl  12738  grpsubadd  12963  grpaddsubass  12965  grpsubsub4  12968  grppnpcan2  12969  grpnpncan  12970  grpnnncan2  12972  mulgnndir  13017  mulgnn0dir  13018  mulgnnass  13023  mulgnn0ass  13024  mulgass  13025  issubg2m  13054  cmn32  13112  cmn12  13114  abladdsub  13123  ablsubsub23  13133  srgdilem  13157  srgass  13159  ringdilem  13200  ringass  13204  opprring  13254  mulgass3  13259  unitgrp  13290  dvrass  13313  dvrdir  13317  subrgunit  13365  issubrg2  13367  aprap  13381  lss1  13454  lsssn0  13461  islss3  13471  restopnb  13766  icnpimaex  13796  cnptopresti  13823  psmettri  13915  isxmet2d  13933  xmettri  13957  metrtri  13962  xmetres2  13964  bldisj  13986  blss2ps  13991  blss2  13992  xmstri2  14055  mstri2  14056  xmstri  14057  mstri  14058  xmstri3  14059  mstri3  14060  msrtri  14061  comet  14084  bdbl  14088  xmetxp  14092  dvconst  14246