Theorem simpl2 991

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

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

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 970

This theorem is referenced by:  simpll2  1027  simprl2  1033  simp1l2  1081  simp2l2  1087  simp3l2  1093  3anandirs  1338  rspc3ev  2846  tfisi  4563  brcogw  4772  oawordi  6433  nnmord  6481  nnmword  6482  ac6sfi  6860  unsnfi  6880  unsnfidcel  6882  ordiso2  6996  prarloclemarch2  7356  enq0tr  7371  distrlem4prl  7521  distrlem4pru  7522  ltaprg  7556  aptiprlemu  7577  lelttr  7983  ltletr  7984  readdcan  8034  addcan  8074  addcan2  8075  ltadd2  8313  ltmul1a  8485  ltmul1  8486  divmulassap  8587  divmulasscomap  8588  lemul1a  8749  xrlelttr  9738  xrltletr  9739  xaddass  9801  xleadd1a  9805  xltadd1  9808  xlesubadd  9815  ixxdisj  9835  icoshftf1o  9923  icodisj  9924  lincmb01cmp  9935  iccf1o  9936  fztri3or  9970  ioom  10192  modqmuladdim  10298  modqmuladdnn0  10299  q2submod  10316  modqaddmulmod  10322  exp3val  10453  ltexp2a  10503  exple1  10507  expnbnd  10574  expnlbnd2  10576  nn0ltexp2  10619  nn0leexp2  10620  expcan  10625  fiprsshashgt1  10726  maxleastb  11152  maxltsup  11156  xrltmaxsup  11194  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  addcn2  11247  mulcn2  11249  geoisum1c  11457  dvdsval2  11726  dvdsmodexp  11731  dvdsadd2b  11776  dvdsmod  11796  oexpneg  11810  divalglemex  11855  divalg  11857  gcdass  11944  rplpwr  11956  rppwr  11957  nnminle  11964  lcmass  12013  coprmdvds2  12021  rpmulgcd2  12023  rpdvds  12027  cncongr2  12032  rpexp  12081  znege1  12106  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  coprimeprodsq2  12186  pythagtriplem3  12195  pythagtriplem4  12196  pcdvdsb  12247  pcbc  12277  ctinf  12359  nninfdc  12382  topssnei  12762  cnptopco  12822  cnconst2  12833  cnptoprest  12839  cnpdis  12842  upxp  12872  bldisj  13001  blgt0  13002  bl2in  13003  blss2ps  13006  blss2  13007  xblm  13017  blssps  13027  blss  13028  xmetresbl  13040  bdbl  13103  bdmopn  13104  metcnp3  13111  metcnp  13112  metcnp2  13113  dvfvalap  13250  dvcnp2cntop  13263  dvcn  13264  logdivlti  13402  ltexp2  13460  lgsfvalg  13506  lgsneg  13525  lgsdilem  13528  lgsdirprm  13535  lgsdir  13536  lgsdi  13538  lgsne0  13539