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  5865  tfrlemibacc  6379  tfrlemibxssdm  6380  tfrlemibfn  6381  tfr1onlembacc  6395  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembxssdm  6409  tfrcllembfn  6410  elfir  7032  prloc  7551  prmuloc2  7627  ltntri  8147  eluzuzle  9600  xlesubadd  9949  elioc2  10002  elico2  10003  elicc2  10004  fseq1p1m1  10160  seq3f1olemp  10586  seq3f1oleml  10587  bcval5  10834  hashdifpr  10891  isumss2  11536  tanaddap  11882  dvds2ln  11967  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  f1ovscpbl  12895  grpsubadd  13160  grpaddsubass  13162  grpsubsub4  13165  grppnpcan2  13166  grpnpncan  13167  grpnnncan2  13169  imasgrp2  13180  imasgrp  13181  mulgnndir  13221  mulgnn0dir  13222  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  issubg2m  13259  qusgrp  13302  kerf1ghm  13344  cmn32  13374  cmn12  13376  abladdsub  13385  ablsubsub23  13395  rngass  13435  imasrng  13452  srgdilem  13465  srgass  13467  ringdilem  13508  ringass  13512  ringrng  13532  imasring  13560  opprrng  13573  opprring  13575  mulgass3  13581  unitgrp  13612  dvrass  13635  dvrdir  13639  subrgunit  13735  issubrg2  13737  aprap  13782  lss1  13858  lsssn0  13866  islss3  13875  sralmod  13946  restopnb  14349  icnpimaex  14379  cnptopresti  14406  psmettri  14498  isxmet2d  14516  xmettri  14540  metrtri  14545  xmetres2  14547  bldisj  14569  blss2ps  14574  blss2  14575  xmstri2  14638  mstri2  14639  xmstri  14640  mstri  14641  xmstri3  14642  mstri3  14643  msrtri  14644  comet  14667  bdbl  14671  xmetxp  14675  dvconst  14846