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  5869  tfrlemibacc  6384  tfrlemibxssdm  6385  tfrlemibfn  6386  tfr1onlembacc  6400  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembxssdm  6414  tfrcllembfn  6415  elfir  7039  prloc  7558  prmuloc2  7634  ltntri  8154  eluzuzle  9609  xlesubadd  9958  elioc2  10011  elico2  10012  elicc2  10013  fseq1p1m1  10169  seq3f1olemp  10607  seq3f1oleml  10608  bcval5  10855  hashdifpr  10912  isumss2  11558  tanaddap  11904  dvds2ln  11989  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  f1ovscpbl  12955  grpsubadd  13220  grpaddsubass  13222  grpsubsub4  13225  grppnpcan2  13226  grpnpncan  13227  grpnnncan2  13229  imasgrp2  13240  imasgrp  13241  mulgnndir  13281  mulgnn0dir  13282  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  issubg2m  13319  qusgrp  13362  kerf1ghm  13404  cmn32  13434  cmn12  13436  abladdsub  13445  ablsubsub23  13455  rngass  13495  imasrng  13512  srgdilem  13525  srgass  13527  ringdilem  13568  ringass  13572  ringrng  13592  imasring  13620  opprrng  13633  opprring  13635  mulgass3  13641  unitgrp  13672  dvrass  13695  dvrdir  13699  subrgunit  13795  issubrg2  13797  aprap  13842  lss1  13918  lsssn0  13926  islss3  13935  sralmod  14006  restopnb  14417  icnpimaex  14447  cnptopresti  14474  psmettri  14566  isxmet2d  14584  xmettri  14608  metrtri  14613  xmetres2  14615  bldisj  14637  blss2ps  14642  blss2  14643  xmstri2  14706  mstri2  14707  xmstri  14708  mstri  14709  xmstri3  14710  mstri3  14711  msrtri  14712  comet  14735  bdbl  14739  xmetxp  14743  dvconst  14930  dvconstre  14932  dvconstss  14934  sgmmul  15232