Theorem simpl2 1027

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

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

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 1006

This theorem is referenced by:  simpll2  1063  simprl2  1069  simp1l2  1117  simp2l2  1123  simp3l2  1129  3anandirs  1384  rspc3ev  2927  ifnetruedc  3649  tfisi  4685  brcogw  4899  oawordi  6636  nnmord  6684  nnmword  6685  1dom1el  6992  ac6sfi  7086  unsnfi  7110  unsnfidcel  7112  ordiso2  7233  prarloclemarch2  7638  enq0tr  7653  distrlem4prl  7803  distrlem4pru  7804  ltaprg  7838  aptiprlemu  7859  lelttr  8267  ltletr  8268  readdcan  8318  addcan  8358  addcan2  8359  ltadd2  8598  ltmul1a  8770  ltmul1  8771  divmulassap  8874  divmulasscomap  8875  lemul1a  9037  xrlelttr  10040  xrltletr  10041  xaddass  10103  xleadd1a  10107  xltadd1  10110  xlesubadd  10117  ixxdisj  10137  icoshftf1o  10225  icodisj  10226  lincmb01cmp  10237  iccf1o  10238  fztri3or  10273  ioom  10519  modqmuladdim  10628  modqmuladdnn0  10629  q2submod  10646  modqaddmulmod  10652  seqp1g  10727  exp3val  10802  ltexp2a  10852  exple1  10856  expnbnd  10924  expnlbnd2  10926  nn0ltexp2  10970  nn0leexp2  10971  mulsubdivbinom2ap  10972  expcan  10977  fiprsshashgt1  11080  fun2dmnop0  11110  ccatass  11184  fzowrddc  11227  swrdclg  11230  ccatopth  11296  pfxccatin12lem2a  11307  maxleastb  11774  maxltsup  11778  xrltmaxsup  11817  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  addcn2  11870  mulcn2  11872  geoisum1c  12080  dvdsval2  12350  dvdsmodexp  12355  dvdsadd2b  12400  dvdsaddre2b  12401  dvdsmod  12422  oexpneg  12437  divalglemex  12482  divalg  12484  gcdass  12585  rplpwr  12597  rppwr  12598  nnminle  12605  lcmass  12656  coprmdvds2  12664  rpmulgcd2  12666  rpdvds  12670  cncongr2  12675  rpexp  12724  znege1  12749  prmdiveq  12807  hashgcdlem  12809  odzdvds  12817  coprimeprodsq2  12830  pythagtriplem3  12839  pythagtriplem4  12840  pcdvdsb  12892  pcbc  12923  ctinf  13050  nninfdc  13073  isnsgrp  13488  issubmnd  13524  nmzsubg  13796  ghmnsgima  13854  srg1zr  13999  ring1eq0  14060  mulgass2  14070  rhmdvdsr  14188  rmodislmod  14364  topssnei  14885  cnptopco  14945  cnconst2  14956  cnptoprest  14962  cnpdis  14965  upxp  14995  bldisj  15124  blgt0  15125  bl2in  15126  blss2ps  15129  blss2  15130  xblm  15140  blssps  15150  blss  15151  xmetresbl  15163  bdbl  15226  bdmopn  15227  metcnp3  15234  metcnp  15235  metcnp2  15236  dvfvalap  15404  dvcnp2cntop  15422  dvcn  15423  ply1term  15466  dvply1  15488  logdivlti  15604  ltexp2  15664  lgsfvalg  15733  lgsneg  15752  lgsdilem  15755  lgsdirprm  15762  lgsdir  15763  lgsdi  15765  lgsne0  15766  clwwlknonex2e  16290