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  5866  tfrlemibacc  6381  tfrlemibxssdm  6382  tfrlemibfn  6383  tfr1onlembacc  6397  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembxssdm  6411  tfrcllembfn  6412  elfir  7034  prloc  7553  prmuloc2  7629  ltntri  8149  eluzuzle  9603  xlesubadd  9952  elioc2  10005  elico2  10006  elicc2  10007  fseq1p1m1  10163  seq3f1olemp  10589  seq3f1oleml  10590  bcval5  10837  hashdifpr  10894  isumss2  11539  tanaddap  11885  dvds2ln  11970  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  f1ovscpbl  12898  grpsubadd  13163  grpaddsubass  13165  grpsubsub4  13168  grppnpcan2  13169  grpnpncan  13170  grpnnncan2  13172  imasgrp2  13183  imasgrp  13184  mulgnndir  13224  mulgnn0dir  13225  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  issubg2m  13262  qusgrp  13305  kerf1ghm  13347  cmn32  13377  cmn12  13379  abladdsub  13388  ablsubsub23  13398  rngass  13438  imasrng  13455  srgdilem  13468  srgass  13470  ringdilem  13511  ringass  13515  ringrng  13535  imasring  13563  opprrng  13576  opprring  13578  mulgass3  13584  unitgrp  13615  dvrass  13638  dvrdir  13642  subrgunit  13738  issubrg2  13740  aprap  13785  lss1  13861  lsssn0  13869  islss3  13878  sralmod  13949  restopnb  14360  icnpimaex  14390  cnptopresti  14417  psmettri  14509  isxmet2d  14527  xmettri  14551  metrtri  14556  xmetres2  14558  bldisj  14580  blss2ps  14585  blss2  14586  xmstri2  14649  mstri2  14650  xmstri  14651  mstri  14652  xmstri3  14653  mstri3  14654  msrtri  14655  comet  14678  bdbl  14682  xmetxp  14686  dvconst  14873  dvconstre  14875  dvconstss  14877