Theorem simpl2 996

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

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

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 975

This theorem is referenced by:  simpll2  1032  simprl2  1038  simp1l2  1086  simp2l2  1092  simp3l2  1098  3anandirs  1343  rspc3ev  2851  tfisi  4571  brcogw  4780  oawordi  6448  nnmord  6496  nnmword  6497  ac6sfi  6876  unsnfi  6896  unsnfidcel  6898  ordiso2  7012  prarloclemarch2  7381  enq0tr  7396  distrlem4prl  7546  distrlem4pru  7547  ltaprg  7581  aptiprlemu  7602  lelttr  8008  ltletr  8009  readdcan  8059  addcan  8099  addcan2  8100  ltadd2  8338  ltmul1a  8510  ltmul1  8511  divmulassap  8612  divmulasscomap  8613  lemul1a  8774  xrlelttr  9763  xrltletr  9764  xaddass  9826  xleadd1a  9830  xltadd1  9833  xlesubadd  9840  ixxdisj  9860  icoshftf1o  9948  icodisj  9949  lincmb01cmp  9960  iccf1o  9961  fztri3or  9995  ioom  10217  modqmuladdim  10323  modqmuladdnn0  10324  q2submod  10341  modqaddmulmod  10347  exp3val  10478  ltexp2a  10528  exple1  10532  expnbnd  10599  expnlbnd2  10601  nn0ltexp2  10644  nn0leexp2  10645  expcan  10650  fiprsshashgt1  10752  maxleastb  11178  maxltsup  11182  xrltmaxsup  11220  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  addcn2  11273  mulcn2  11275  geoisum1c  11483  dvdsval2  11752  dvdsmodexp  11757  dvdsadd2b  11802  dvdsmod  11822  oexpneg  11836  divalglemex  11881  divalg  11883  gcdass  11970  rplpwr  11982  rppwr  11983  nnminle  11990  lcmass  12039  coprmdvds2  12047  rpmulgcd2  12049  rpdvds  12053  cncongr2  12058  rpexp  12107  znege1  12132  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  coprimeprodsq2  12212  pythagtriplem3  12221  pythagtriplem4  12222  pcdvdsb  12273  pcbc  12303  ctinf  12385  nninfdc  12408  isnsgrp  12647  topssnei  12956  cnptopco  13016  cnconst2  13027  cnptoprest  13033  cnpdis  13036  upxp  13066  bldisj  13195  blgt0  13196  bl2in  13197  blss2ps  13200  blss2  13201  xblm  13211  blssps  13221  blss  13222  xmetresbl  13234  bdbl  13297  bdmopn  13298  metcnp3  13305  metcnp  13306  metcnp2  13307  dvfvalap  13444  dvcnp2cntop  13457  dvcn  13458  logdivlti  13596  ltexp2  13654  lgsfvalg  13700  lgsneg  13719  lgsdilem  13722  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgsne0  13733