Theorem simpl2 986

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

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

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 965

This theorem is referenced by:  simpll2  1022  simprl2  1028  simp1l2  1076  simp2l2  1082  simp3l2  1088  3anandirs  1330  rspc3ev  2833  tfisi  4547  brcogw  4756  oawordi  6417  nnmord  6465  nnmword  6466  ac6sfi  6844  unsnfi  6864  unsnfidcel  6866  ordiso2  6980  prarloclemarch2  7340  enq0tr  7355  distrlem4prl  7505  distrlem4pru  7506  ltaprg  7540  aptiprlemu  7561  lelttr  7966  ltletr  7967  readdcan  8016  addcan  8056  addcan2  8057  ltadd2  8295  ltmul1a  8467  ltmul1  8468  divmulassap  8569  divmulasscomap  8570  lemul1a  8730  xrlelttr  9711  xrltletr  9712  xaddass  9774  xleadd1a  9778  xltadd1  9781  xlesubadd  9788  ixxdisj  9808  icoshftf1o  9896  icodisj  9897  lincmb01cmp  9908  iccf1o  9909  fztri3or  9942  ioom  10164  modqmuladdim  10270  modqmuladdnn0  10271  q2submod  10288  modqaddmulmod  10294  exp3val  10425  ltexp2a  10475  exple1  10479  expnbnd  10545  expnlbnd2  10547  expcan  10594  fiprsshashgt1  10695  maxleastb  11118  maxltsup  11122  xrltmaxsup  11158  xrmaxltsup  11159  xrmaxaddlem  11161  xrmaxadd  11162  addcn2  11211  mulcn2  11213  geoisum1c  11421  dvdsval2  11690  dvdsmodexp  11695  dvdsadd2b  11738  dvdsmod  11758  oexpneg  11772  divalglemex  11817  divalg  11819  gcdass  11903  rplpwr  11915  rppwr  11916  lcmass  11966  coprmdvds2  11974  rpmulgcd2  11976  rpdvds  11980  cncongr2  11985  rpexp  12032  znege1  12057  prmdiveq  12115  hashgcdlem  12117  odzdvds  12124  coprimeprodsq2  12137  pythagtriplem3  12146  pythagtriplem4  12147  ctinf  12201  nnminle  12220  nninfdc  12226  topssnei  12604  cnptopco  12664  cnconst2  12675  cnptoprest  12681  cnpdis  12684  upxp  12714  bldisj  12843  blgt0  12844  bl2in  12845  blss2ps  12848  blss2  12849  xblm  12859  blssps  12869  blss  12870  xmetresbl  12882  bdbl  12945  bdmopn  12946  metcnp3  12953  metcnp  12954  metcnp2  12955  dvfvalap  13092  dvcnp2cntop  13105  dvcn  13106  logdivlti  13244