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  3602  tfisi  4623  brcogw  4835  oawordi  6527  nnmord  6575  nnmword  6576  ac6sfi  6959  unsnfi  6980  unsnfidcel  6982  ordiso2  7101  prarloclemarch2  7486  enq0tr  7501  distrlem4prl  7651  distrlem4pru  7652  ltaprg  7686  aptiprlemu  7707  lelttr  8115  ltletr  8116  readdcan  8166  addcan  8206  addcan2  8207  ltadd2  8446  ltmul1a  8618  ltmul1  8619  divmulassap  8722  divmulasscomap  8723  lemul1a  8885  xrlelttr  9881  xrltletr  9882  xaddass  9944  xleadd1a  9948  xltadd1  9951  xlesubadd  9958  ixxdisj  9978  icoshftf1o  10066  icodisj  10067  lincmb01cmp  10078  iccf1o  10079  fztri3or  10114  ioom  10350  modqmuladdim  10459  modqmuladdnn0  10460  q2submod  10477  modqaddmulmod  10483  seqp1g  10558  exp3val  10633  ltexp2a  10683  exple1  10687  expnbnd  10755  expnlbnd2  10757  nn0ltexp2  10801  nn0leexp2  10802  mulsubdivbinom2ap  10803  expcan  10808  fiprsshashgt1  10909  maxleastb  11379  maxltsup  11383  xrltmaxsup  11422  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  addcn2  11475  mulcn2  11477  geoisum1c  11685  dvdsval2  11955  dvdsmodexp  11960  dvdsadd2b  12005  dvdsaddre2b  12006  dvdsmod  12027  oexpneg  12042  divalglemex  12087  divalg  12089  gcdass  12182  rplpwr  12194  rppwr  12195  nnminle  12202  lcmass  12253  coprmdvds2  12261  rpmulgcd2  12263  rpdvds  12267  cncongr2  12272  rpexp  12321  znege1  12346  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  coprimeprodsq2  12427  pythagtriplem3  12436  pythagtriplem4  12437  pcdvdsb  12489  pcbc  12520  ctinf  12647  nninfdc  12670  isnsgrp  13049  issubmnd  13083  nmzsubg  13340  ghmnsgima  13398  srg1zr  13543  ring1eq0  13604  mulgass2  13614  rhmdvdsr  13731  rmodislmod  13907  topssnei  14398  cnptopco  14458  cnconst2  14469  cnptoprest  14475  cnpdis  14478  upxp  14508  bldisj  14637  blgt0  14638  bl2in  14639  blss2ps  14642  blss2  14643  xblm  14653  blssps  14663  blss  14664  xmetresbl  14676  bdbl  14739  bdmopn  14740  metcnp3  14747  metcnp  14748  metcnp2  14749  dvfvalap  14917  dvcnp2cntop  14935  dvcn  14936  ply1term  14979  dvply1  15001  logdivlti  15117  ltexp2  15177  lgsfvalg  15246  lgsneg  15265  lgsdilem  15268  lgsdirprm  15275  lgsdir  15276  lgsdi  15278  lgsne0  15279  1dom1el  15637