Theorem simpr3 1007

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 1001	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

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

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 982

This theorem is referenced by:  simplr3  1043  simprr3  1049  simp1r3  1097  simp2r3  1103  simp3r3  1109  3anandis  1358  isopolem  5872  tfrlemibacc  6393  tfrlemibxssdm  6394  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembxssdm  6423  tfrcllembfn  6424  elfir  7048  prloc  7575  prmuloc2  7651  ltntri  8171  eluzuzle  9626  xlesubadd  9975  elioc2  10028  elico2  10029  elicc2  10030  fseq1p1m1  10186  seq3f1olemp  10624  seq3f1oleml  10625  bcval5  10872  hashdifpr  10929  isumss2  11575  tanaddap  11921  dvds2ln  12006  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  f1ovscpbl  13014  prdssgrpd  13117  prdsmndd  13150  imasmnd2  13154  imasmnd  13155  grpsubadd  13290  grpaddsubass  13292  grpsubsub4  13295  grppnpcan2  13296  grpnpncan  13297  grpnnncan2  13299  imasgrp2  13316  imasgrp  13317  mulgnndir  13357  mulgnn0dir  13358  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  issubg2m  13395  qusgrp  13438  kerf1ghm  13480  cmn32  13510  cmn12  13512  abladdsub  13521  ablsubsub23  13531  rngass  13571  imasrng  13588  srgdilem  13601  srgass  13603  ringdilem  13644  ringass  13648  ringrng  13668  imasring  13696  opprrng  13709  opprring  13711  mulgass3  13717  unitgrp  13748  dvrass  13771  dvrdir  13775  subrgunit  13871  issubrg2  13873  aprap  13918  lss1  13994  lsssn0  14002  islss3  14011  sralmod  14082  restopnb  14501  icnpimaex  14531  cnptopresti  14558  psmettri  14650  isxmet2d  14668  xmettri  14692  metrtri  14697  xmetres2  14699  bldisj  14721  blss2ps  14726  blss2  14727  xmstri2  14790  mstri2  14791  xmstri  14792  mstri  14793  xmstri3  14794  mstri3  14795  msrtri  14796  comet  14819  bdbl  14823  xmetxp  14827  dvconst  15014  dvconstre  15016  dvconstss  15018  sgmmul  15316