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  2885  ifnetruedc  3603  tfisi  4624  brcogw  4836  oawordi  6536  nnmord  6584  nnmword  6585  ac6sfi  6968  unsnfi  6989  unsnfidcel  6991  ordiso2  7110  prarloclemarch2  7503  enq0tr  7518  distrlem4prl  7668  distrlem4pru  7669  ltaprg  7703  aptiprlemu  7724  lelttr  8132  ltletr  8133  readdcan  8183  addcan  8223  addcan2  8224  ltadd2  8463  ltmul1a  8635  ltmul1  8636  divmulassap  8739  divmulasscomap  8740  lemul1a  8902  xrlelttr  9898  xrltletr  9899  xaddass  9961  xleadd1a  9965  xltadd1  9968  xlesubadd  9975  ixxdisj  9995  icoshftf1o  10083  icodisj  10084  lincmb01cmp  10095  iccf1o  10096  fztri3or  10131  ioom  10367  modqmuladdim  10476  modqmuladdnn0  10477  q2submod  10494  modqaddmulmod  10500  seqp1g  10575  exp3val  10650  ltexp2a  10700  exple1  10704  expnbnd  10772  expnlbnd2  10774  nn0ltexp2  10818  nn0leexp2  10819  mulsubdivbinom2ap  10820  expcan  10825  fiprsshashgt1  10926  maxleastb  11396  maxltsup  11400  xrltmaxsup  11439  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  addcn2  11492  mulcn2  11494  geoisum1c  11702  dvdsval2  11972  dvdsmodexp  11977  dvdsadd2b  12022  dvdsaddre2b  12023  dvdsmod  12044  oexpneg  12059  divalglemex  12104  divalg  12106  gcdass  12207  rplpwr  12219  rppwr  12220  nnminle  12227  lcmass  12278  coprmdvds2  12286  rpmulgcd2  12288  rpdvds  12292  cncongr2  12297  rpexp  12346  znege1  12371  prmdiveq  12429  hashgcdlem  12431  odzdvds  12439  coprimeprodsq2  12452  pythagtriplem3  12461  pythagtriplem4  12462  pcdvdsb  12514  pcbc  12545  ctinf  12672  nninfdc  12695  isnsgrp  13108  issubmnd  13144  nmzsubg  13416  ghmnsgima  13474  srg1zr  13619  ring1eq0  13680  mulgass2  13690  rhmdvdsr  13807  rmodislmod  13983  topssnei  14482  cnptopco  14542  cnconst2  14553  cnptoprest  14559  cnpdis  14562  upxp  14592  bldisj  14721  blgt0  14722  bl2in  14723  blss2ps  14726  blss2  14727  xblm  14737  blssps  14747  blss  14748  xmetresbl  14760  bdbl  14823  bdmopn  14824  metcnp3  14831  metcnp  14832  metcnp2  14833  dvfvalap  15001  dvcnp2cntop  15019  dvcn  15020  ply1term  15063  dvply1  15085  logdivlti  15201  ltexp2  15261  lgsfvalg  15330  lgsneg  15349  lgsdilem  15352  lgsdirprm  15359  lgsdir  15360  lgsdi  15362  lgsne0  15363  1dom1el  15721