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  1359  isopolem  5890  tfrlemibacc  6411  tfrlemibxssdm  6412  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembxssdm  6441  tfrcllembfn  6442  elfir  7074  prloc  7603  prmuloc2  7679  ltntri  8199  eluzuzle  9655  xlesubadd  10004  elioc2  10057  elico2  10058  elicc2  10059  fseq1p1m1  10215  seq3f1olemp  10658  seq3f1oleml  10659  bcval5  10906  hashdifpr  10963  isumss2  11675  tanaddap  12021  dvds2ln  12106  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  f1ovscpbl  13115  prdssgrpd  13218  prdsmndd  13251  imasmnd2  13255  imasmnd  13256  grpsubadd  13391  grpaddsubass  13393  grpsubsub4  13396  grppnpcan2  13397  grpnpncan  13398  grpnnncan2  13400  imasgrp2  13417  imasgrp  13418  mulgnndir  13458  mulgnn0dir  13459  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  issubg2m  13496  qusgrp  13539  kerf1ghm  13581  cmn32  13611  cmn12  13613  abladdsub  13622  ablsubsub23  13632  rngass  13672  imasrng  13689  srgdilem  13702  srgass  13704  ringdilem  13745  ringass  13749  ringrng  13769  imasring  13797  opprrng  13810  opprring  13812  mulgass3  13818  unitgrp  13849  dvrass  13872  dvrdir  13876  subrgunit  13972  issubrg2  13974  aprap  14019  lss1  14095  lsssn0  14103  islss3  14112  sralmod  14183  restopnb  14624  icnpimaex  14654  cnptopresti  14681  psmettri  14773  isxmet2d  14791  xmettri  14815  metrtri  14820  xmetres2  14822  bldisj  14844  blss2ps  14849  blss2  14850  xmstri2  14913  mstri2  14914  xmstri  14915  mstri  14916  xmstri3  14917  mstri3  14918  msrtri  14919  comet  14942  bdbl  14946  xmetxp  14950  dvconst  15137  dvconstre  15139  dvconstss  15141  sgmmul  15439