Theorem simpl2 1001

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

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

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 980

This theorem is referenced by:  simpll2  1037  simprl2  1043  simp1l2  1091  simp2l2  1097  simp3l2  1103  3anandirs  1348  rspc3ev  2860  tfisi  4588  brcogw  4798  oawordi  6473  nnmord  6521  nnmword  6522  ac6sfi  6901  unsnfi  6921  unsnfidcel  6923  ordiso2  7037  prarloclemarch2  7421  enq0tr  7436  distrlem4prl  7586  distrlem4pru  7587  ltaprg  7621  aptiprlemu  7642  lelttr  8049  ltletr  8050  readdcan  8100  addcan  8140  addcan2  8141  ltadd2  8379  ltmul1a  8551  ltmul1  8552  divmulassap  8655  divmulasscomap  8656  lemul1a  8818  xrlelttr  9809  xrltletr  9810  xaddass  9872  xleadd1a  9876  xltadd1  9879  xlesubadd  9886  ixxdisj  9906  icoshftf1o  9994  icodisj  9995  lincmb01cmp  10006  iccf1o  10007  fztri3or  10042  ioom  10264  modqmuladdim  10370  modqmuladdnn0  10371  q2submod  10388  modqaddmulmod  10394  exp3val  10525  ltexp2a  10575  exple1  10579  expnbnd  10647  expnlbnd2  10649  nn0ltexp2  10692  nn0leexp2  10693  mulsubdivbinom2ap  10694  expcan  10699  fiprsshashgt1  10800  maxleastb  11226  maxltsup  11230  xrltmaxsup  11268  xrmaxltsup  11269  xrmaxaddlem  11271  xrmaxadd  11272  addcn2  11321  mulcn2  11323  geoisum1c  11531  dvdsval2  11800  dvdsmodexp  11805  dvdsadd2b  11850  dvdsaddre2b  11851  dvdsmod  11871  oexpneg  11885  divalglemex  11930  divalg  11932  gcdass  12019  rplpwr  12031  rppwr  12032  nnminle  12039  lcmass  12088  coprmdvds2  12096  rpmulgcd2  12098  rpdvds  12102  cncongr2  12107  rpexp  12156  znege1  12181  prmdiveq  12239  hashgcdlem  12241  odzdvds  12248  coprimeprodsq2  12261  pythagtriplem3  12270  pythagtriplem4  12271  pcdvdsb  12322  pcbc  12352  ctinf  12434  nninfdc  12457  isnsgrp  12819  issubmnd  12850  nmzsubg  13080  srg1zr  13181  ring1eq0  13236  mulgass2  13246  rmodislmod  13452  topssnei  13823  cnptopco  13883  cnconst2  13894  cnptoprest  13900  cnpdis  13903  upxp  13933  bldisj  14062  blgt0  14063  bl2in  14064  blss2ps  14067  blss2  14068  xblm  14078  blssps  14088  blss  14089  xmetresbl  14101  bdbl  14164  bdmopn  14165  metcnp3  14172  metcnp  14173  metcnp2  14174  dvfvalap  14311  dvcnp2cntop  14324  dvcn  14325  logdivlti  14463  ltexp2  14521  lgsfvalg  14567  lgsneg  14586  lgsdilem  14589  lgsdirprm  14596  lgsdir  14597  lgsdi  14599  lgsne0  14600  1dom1el  14904