Theorem simpl2 947

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 944	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
2	1	adantr 270	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  simpll2  983  simprl2  989  simp1l2  1037  simp2l2  1043  simp3l2  1049  3anandirs  1284  rspc3ev  2738  tfisi  4402  brcogw  4605  oawordi  6230  nnmord  6276  nnmword  6277  ac6sfi  6614  unsnfi  6629  unsnfidcel  6631  ordiso2  6728  prarloclemarch2  6978  enq0tr  6993  distrlem4prl  7143  distrlem4pru  7144  ltaprg  7178  aptiprlemu  7199  lelttr  7573  ltletr  7574  readdcan  7622  addcan  7662  addcan2  7663  ltadd2  7897  ltmul1a  8068  ltmul1  8069  divmulassap  8162  divmulasscomap  8163  lemul1a  8319  xrlelttr  9271  xrltletr  9272  ixxdisj  9321  icoshftf1o  9408  icodisj  9409  lincmb01cmp  9420  iccf1o  9421  fztri3or  9453  ioom  9672  modqmuladdim  9774  modqmuladdnn0  9775  q2submod  9792  modqaddmulmod  9798  exp3val  9957  ltexp2a  10007  exple1  10011  expnbnd  10077  expnlbnd2  10079  expcan  10125  fiprsshashgt1  10225  maxleastb  10647  maxltsup  10651  addcn2  10699  mulcn2  10701  geoisum1c  10914  dvdsval2  11077  dvdsadd2b  11121  dvdsmod  11141  oexpneg  11155  divalglemex  11200  divalg  11202  gcdass  11282  rplpwr  11294  rppwr  11295  lcmass  11345  coprmdvds2  11353  rpmulgcd2  11355  rpdvds  11359  cncongr2  11364  rpexp  11410  znege1  11434  hashgcdlem  11481