Theorem simpl2 985

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl2	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simp2 982	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
2	1	adantr 274	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpll2  1021  simprl2  1027  simp1l2  1075  simp2l2  1081  simp3l2  1087  3anandirs  1326  rspc3ev  2806  tfisi  4501  brcogw  4708  oawordi  6365  nnmord  6413  nnmword  6414  ac6sfi  6792  unsnfi  6807  unsnfidcel  6809  ordiso2  6920  prarloclemarch2  7227  enq0tr  7242  distrlem4prl  7392  distrlem4pru  7393  ltaprg  7427  aptiprlemu  7448  lelttr  7852  ltletr  7853  readdcan  7902  addcan  7942  addcan2  7943  ltadd2  8181  ltmul1a  8353  ltmul1  8354  divmulassap  8455  divmulasscomap  8456  lemul1a  8616  xrlelttr  9589  xrltletr  9590  xaddass  9652  xleadd1a  9656  xltadd1  9659  xlesubadd  9666  ixxdisj  9686  icoshftf1o  9774  icodisj  9775  lincmb01cmp  9786  iccf1o  9787  fztri3or  9819  ioom  10038  modqmuladdim  10140  modqmuladdnn0  10141  q2submod  10158  modqaddmulmod  10164  exp3val  10295  ltexp2a  10345  exple1  10349  expnbnd  10415  expnlbnd2  10417  expcan  10463  fiprsshashgt1  10563  maxleastb  10986  maxltsup  10990  xrltmaxsup  11026  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  addcn2  11079  mulcn2  11081  geoisum1c  11289  dvdsval2  11496  dvdsadd2b  11540  dvdsmod  11560  oexpneg  11574  divalglemex  11619  divalg  11621  gcdass  11703  rplpwr  11715  rppwr  11716  lcmass  11766  coprmdvds2  11774  rpmulgcd2  11776  rpdvds  11780  cncongr2  11785  rpexp  11831  znege1  11856  hashgcdlem  11903  ctinf  11943  topssnei  12331  cnptopco  12391  cnconst2  12402  cnptoprest  12408  cnpdis  12411  upxp  12441  bldisj  12570  blgt0  12571  bl2in  12572  blss2ps  12575  blss2  12576  xblm  12586  blssps  12596  blss  12597  xmetresbl  12609  bdbl  12672  bdmopn  12673  metcnp3  12680  metcnp  12681  metcnp2  12682  dvfvalap  12819  dvcnp2cntop  12832  dvcn  12833