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  1360  rspc3ev  2893  ifnetruedc  3612  tfisi  4634  brcogw  4846  oawordi  6554  nnmord  6602  nnmword  6603  ac6sfi  6994  unsnfi  7015  unsnfidcel  7017  ordiso2  7136  prarloclemarch2  7531  enq0tr  7546  distrlem4prl  7696  distrlem4pru  7697  ltaprg  7731  aptiprlemu  7752  lelttr  8160  ltletr  8161  readdcan  8211  addcan  8251  addcan2  8252  ltadd2  8491  ltmul1a  8663  ltmul1  8664  divmulassap  8767  divmulasscomap  8768  lemul1a  8930  xrlelttr  9927  xrltletr  9928  xaddass  9990  xleadd1a  9994  xltadd1  9997  xlesubadd  10004  ixxdisj  10024  icoshftf1o  10112  icodisj  10113  lincmb01cmp  10124  iccf1o  10125  fztri3or  10160  ioom  10401  modqmuladdim  10510  modqmuladdnn0  10511  q2submod  10528  modqaddmulmod  10534  seqp1g  10609  exp3val  10684  ltexp2a  10734  exple1  10738  expnbnd  10806  expnlbnd2  10808  nn0ltexp2  10852  nn0leexp2  10853  mulsubdivbinom2ap  10854  expcan  10859  fiprsshashgt1  10960  fun2dmnop0  10990  ccatass  11062  maxleastb  11467  maxltsup  11471  xrltmaxsup  11510  xrmaxltsup  11511  xrmaxaddlem  11513  xrmaxadd  11514  addcn2  11563  mulcn2  11565  geoisum1c  11773  dvdsval2  12043  dvdsmodexp  12048  dvdsadd2b  12093  dvdsaddre2b  12094  dvdsmod  12115  oexpneg  12130  divalglemex  12175  divalg  12177  gcdass  12278  rplpwr  12290  rppwr  12291  nnminle  12298  lcmass  12349  coprmdvds2  12357  rpmulgcd2  12359  rpdvds  12363  cncongr2  12368  rpexp  12417  znege1  12442  prmdiveq  12500  hashgcdlem  12502  odzdvds  12510  coprimeprodsq2  12523  pythagtriplem3  12532  pythagtriplem4  12533  pcdvdsb  12585  pcbc  12616  ctinf  12743  nninfdc  12766  isnsgrp  13180  issubmnd  13216  nmzsubg  13488  ghmnsgima  13546  srg1zr  13691  ring1eq0  13752  mulgass2  13762  rhmdvdsr  13879  rmodislmod  14055  topssnei  14576  cnptopco  14636  cnconst2  14647  cnptoprest  14653  cnpdis  14656  upxp  14686  bldisj  14815  blgt0  14816  bl2in  14817  blss2ps  14820  blss2  14821  xblm  14831  blssps  14841  blss  14842  xmetresbl  14854  bdbl  14917  bdmopn  14918  metcnp3  14925  metcnp  14926  metcnp2  14927  dvfvalap  15095  dvcnp2cntop  15113  dvcn  15114  ply1term  15157  dvply1  15179  logdivlti  15295  ltexp2  15355  lgsfvalg  15424  lgsneg  15443  lgsdilem  15446  lgsdirprm  15453  lgsdir  15454  lgsdi  15456  lgsne0  15457  1dom1el  15860