Theorem simpl2 1003

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpll2  1039  simprl2  1045  simp1l2  1093  simp2l2  1099  simp3l2  1105  3anandirs  1359  rspc3ev  2881  ifnetruedc  3598  tfisi  4619  brcogw  4831  oawordi  6522  nnmord  6570  nnmword  6571  ac6sfi  6954  unsnfi  6975  unsnfidcel  6977  ordiso2  7094  prarloclemarch2  7479  enq0tr  7494  distrlem4prl  7644  distrlem4pru  7645  ltaprg  7679  aptiprlemu  7700  lelttr  8108  ltletr  8109  readdcan  8159  addcan  8199  addcan2  8200  ltadd2  8438  ltmul1a  8610  ltmul1  8611  divmulassap  8714  divmulasscomap  8715  lemul1a  8877  xrlelttr  9872  xrltletr  9873  xaddass  9935  xleadd1a  9939  xltadd1  9942  xlesubadd  9949  ixxdisj  9969  icoshftf1o  10057  icodisj  10058  lincmb01cmp  10069  iccf1o  10070  fztri3or  10105  ioom  10329  modqmuladdim  10438  modqmuladdnn0  10439  q2submod  10456  modqaddmulmod  10462  seqp1g  10537  exp3val  10612  ltexp2a  10662  exple1  10666  expnbnd  10734  expnlbnd2  10736  nn0ltexp2  10780  nn0leexp2  10781  mulsubdivbinom2ap  10782  expcan  10787  fiprsshashgt1  10888  maxleastb  11358  maxltsup  11362  xrltmaxsup  11400  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  addcn2  11453  mulcn2  11455  geoisum1c  11663  dvdsval2  11933  dvdsmodexp  11938  dvdsadd2b  11983  dvdsaddre2b  11984  dvdsmod  12004  oexpneg  12018  divalglemex  12063  divalg  12065  gcdass  12152  rplpwr  12164  rppwr  12165  nnminle  12172  lcmass  12223  coprmdvds2  12231  rpmulgcd2  12233  rpdvds  12237  cncongr2  12242  rpexp  12291  znege1  12316  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  coprimeprodsq2  12396  pythagtriplem3  12405  pythagtriplem4  12406  pcdvdsb  12458  pcbc  12489  ctinf  12587  nninfdc  12610  isnsgrp  12989  issubmnd  13023  nmzsubg  13280  ghmnsgima  13338  srg1zr  13483  ring1eq0  13544  mulgass2  13554  rhmdvdsr  13671  rmodislmod  13847  topssnei  14330  cnptopco  14390  cnconst2  14401  cnptoprest  14407  cnpdis  14410  upxp  14440  bldisj  14569  blgt0  14570  bl2in  14571  blss2ps  14574  blss2  14575  xblm  14585  blssps  14595  blss  14596  xmetresbl  14608  bdbl  14671  bdmopn  14672  metcnp3  14679  metcnp  14680  metcnp2  14681  dvfvalap  14835  dvcnp2cntop  14848  dvcn  14849  ply1term  14889  logdivlti  15016  ltexp2  15074  lgsfvalg  15121  lgsneg  15140  lgsdilem  15143  lgsdirprm  15150  lgsdir  15151  lgsdi  15153  lgsne0  15154  1dom1el  15483