Theorem simpr3 1008

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

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

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 983

This theorem is referenced by:  simplr3  1044  simprr3  1050  simp1r3  1098  simp2r3  1104  simp3r3  1110  3anandis  1360  isopolem  5914  tfrlemibacc  6435  tfrlemibxssdm  6436  tfrlemibfn  6437  tfr1onlembacc  6451  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfrcllembacc  6464  tfrcllembxssdm  6465  tfrcllembfn  6466  elfir  7101  prloc  7639  prmuloc2  7715  ltntri  8235  eluzuzle  9691  xlesubadd  10040  elioc2  10093  elico2  10094  elicc2  10095  fseq1p1m1  10251  seq3f1olemp  10697  seq3f1oleml  10698  bcval5  10945  hashdifpr  11002  ccatswrd  11161  pfxccat3a  11229  isumss2  11819  tanaddap  12165  dvds2ln  12250  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  f1ovscpbl  13259  prdssgrpd  13362  prdsmndd  13395  imasmnd2  13399  imasmnd  13400  grpsubadd  13535  grpaddsubass  13537  grpsubsub4  13540  grppnpcan2  13541  grpnpncan  13542  grpnnncan2  13544  imasgrp2  13561  imasgrp  13562  mulgnndir  13602  mulgnn0dir  13603  mulgnnass  13608  mulgnn0ass  13609  mulgass  13610  issubg2m  13640  qusgrp  13683  kerf1ghm  13725  cmn32  13755  cmn12  13757  abladdsub  13766  ablsubsub23  13776  rngass  13816  imasrng  13833  srgdilem  13846  srgass  13848  ringdilem  13889  ringass  13893  ringrng  13913  imasring  13941  opprrng  13954  opprring  13956  mulgass3  13962  unitgrp  13993  dvrass  14016  dvrdir  14020  subrgunit  14116  issubrg2  14118  aprap  14163  lss1  14239  lsssn0  14247  islss3  14256  sralmod  14327  restopnb  14768  icnpimaex  14798  cnptopresti  14825  psmettri  14917  isxmet2d  14935  xmettri  14959  metrtri  14964  xmetres2  14966  bldisj  14988  blss2ps  14993  blss2  14994  xmstri2  15057  mstri2  15058  xmstri  15059  mstri  15060  xmstri3  15061  mstri3  15062  msrtri  15063  comet  15086  bdbl  15090  xmetxp  15094  dvconst  15281  dvconstre  15283  dvconstss  15285  sgmmul  15583