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  11496  maxltsup  11500  xrltmaxsup  11539  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  addcn2  11592  mulcn2  11594  geoisum1c  11802  dvdsval2  12072  dvdsmodexp  12077  dvdsadd2b  12122  dvdsaddre2b  12123  dvdsmod  12144  oexpneg  12159  divalglemex  12204  divalg  12206  gcdass  12307  rplpwr  12319  rppwr  12320  nnminle  12327  lcmass  12378  coprmdvds2  12386  rpmulgcd2  12388  rpdvds  12392  cncongr2  12397  rpexp  12446  znege1  12471  prmdiveq  12529  hashgcdlem  12531  odzdvds  12539  coprimeprodsq2  12552  pythagtriplem3  12561  pythagtriplem4  12562  pcdvdsb  12614  pcbc  12645  ctinf  12772  nninfdc  12795  isnsgrp  13209  issubmnd  13245  nmzsubg  13517  ghmnsgima  13575  srg1zr  13720  ring1eq0  13781  mulgass2  13791  rhmdvdsr  13908  rmodislmod  14084  topssnei  14605  cnptopco  14665  cnconst2  14676  cnptoprest  14682  cnpdis  14685  upxp  14715  bldisj  14844  blgt0  14845  bl2in  14846  blss2ps  14849  blss2  14850  xblm  14860  blssps  14870  blss  14871  xmetresbl  14883  bdbl  14946  bdmopn  14947  metcnp3  14954  metcnp  14955  metcnp2  14956  dvfvalap  15124  dvcnp2cntop  15142  dvcn  15143  ply1term  15186  dvply1  15208  logdivlti  15324  ltexp2  15384  lgsfvalg  15453  lgsneg  15472  lgsdilem  15475  lgsdirprm  15482  lgsdir  15483  lgsdi  15485  lgsne0  15486  1dom1el  15889