Theorem simpl2 942

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

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

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 921

This theorem is referenced by:  simpll2  978  simprl2  984  simp1l2  1032  simp2l2  1038  simp3l2  1044  3anandirs  1279  rspc3ev  2717  tfisi  4328  brcogw  4522  oawordi  6072  nnmord  6113  nnmword  6114  ac6sfi  6379  unsnfi  6384  unsnfidcel  6386  ordiso2  6446  prarloclemarch2  6609  enq0tr  6624  distrlem4prl  6774  distrlem4pru  6775  ltaprg  6809  aptiprlemu  6830  lelttr  7199  ltletr  7200  readdcan  7248  addcan  7288  addcan2  7289  ltadd2  7523  ltmul1a  7691  ltmul1  7692  divmulassap  7783  divmulasscomap  7784  lemul1a  7936  xrlelttr  8876  xrltletr  8877  ixxdisj  8926  icoshftf1o  9013  icodisj  9014  lincmb01cmp  9025  iccf1o  9026  fztri3or  9058  ioom  9269  modqmuladdim  9369  modqmuladdnn0  9370  q2submod  9387  modqaddmulmod  9393  ltexp2a  9528  exple1  9532  expnbnd  9596  expnlbnd2  9598  expcan  9644  maxleastb  10100  maxltsup  10104  addcn2  10149  mulcn2  10151  dvdsval2  10198  dvdsadd2b  10242  dvdsmod  10262  oexpneg  10276  divalglemex  10322  divalg  10324  gcdass  10404  rplpwr  10416  rppwr  10417  lcmass  10467  coprmdvds2  10475  rpmulgcd2  10477  rpdvds  10481  cncongr2  10486  rpexp  10532  znege1  10556