Theorem simpr3 1031

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

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

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 1006

This theorem is referenced by:  simplr3  1067  simprr3  1073  simp1r3  1121  simp2r3  1127  simp3r3  1133  3anandis  1383  isopolem  5963  tfrlemibacc  6492  tfrlemibxssdm  6493  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembxssdm  6522  tfrcllembfn  6523  elfir  7172  prloc  7711  prmuloc2  7787  ltntri  8307  eluzuzle  9764  xlesubadd  10118  elioc2  10171  elico2  10172  elicc2  10173  fseq1p1m1  10329  seq3f1olemp  10778  seq3f1oleml  10779  bcval5  11026  hashdifpr  11085  hashtpgim  11110  ccatswrd  11255  pfxccat3a  11323  isumss2  11972  tanaddap  12318  dvds2ln  12403  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  f1ovscpbl  13413  prdssgrpd  13516  prdsmndd  13549  imasmnd2  13553  imasmnd  13554  grpsubadd  13689  grpaddsubass  13691  grpsubsub4  13694  grppnpcan2  13695  grpnpncan  13696  grpnnncan2  13698  imasgrp2  13715  imasgrp  13716  mulgnndir  13756  mulgnn0dir  13757  mulgnnass  13762  mulgnn0ass  13763  mulgass  13764  issubg2m  13794  qusgrp  13837  kerf1ghm  13879  cmn32  13909  cmn12  13911  abladdsub  13920  ablsubsub23  13930  rngass  13971  imasrng  13988  srgdilem  14001  srgass  14003  ringdilem  14044  ringass  14048  ringrng  14068  imasring  14096  opprrng  14109  opprring  14111  mulgass3  14117  unitgrp  14149  dvrass  14172  dvrdir  14176  subrgunit  14272  issubrg2  14274  aprap  14319  lss1  14395  lsssn0  14403  islss3  14412  sralmod  14483  restopnb  14924  icnpimaex  14954  cnptopresti  14981  psmettri  15073  isxmet2d  15091  xmettri  15115  metrtri  15120  xmetres2  15122  bldisj  15144  blss2ps  15149  blss2  15150  xmstri2  15213  mstri2  15214  xmstri  15215  mstri  15216  xmstri3  15217  mstri3  15218  msrtri  15219  comet  15242  bdbl  15246  xmetxp  15250  dvconst  15437  dvconstre  15439  dvconstss  15441  sgmmul  15739  pw1ndom3  16640