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  7505  enq0tr  7520  distrlem4prl  7670  distrlem4pru  7671  ltaprg  7705  aptiprlemu  7726  lelttr  8134  ltletr  8135  readdcan  8185  addcan  8225  addcan2  8226  ltadd2  8465  ltmul1a  8637  ltmul1  8638  divmulassap  8741  divmulasscomap  8742  lemul1a  8904  xrlelttr  9900  xrltletr  9901  xaddass  9963  xleadd1a  9967  xltadd1  9970  xlesubadd  9977  ixxdisj  9997  icoshftf1o  10085  icodisj  10086  lincmb01cmp  10097  iccf1o  10098  fztri3or  10133  ioom  10369  modqmuladdim  10478  modqmuladdnn0  10479  q2submod  10496  modqaddmulmod  10502  seqp1g  10577  exp3val  10652  ltexp2a  10702  exple1  10706  expnbnd  10774  expnlbnd2  10776  nn0ltexp2  10820  nn0leexp2  10821  mulsubdivbinom2ap  10822  expcan  10827  fiprsshashgt1  10928  maxleastb  11398  maxltsup  11402  xrltmaxsup  11441  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  addcn2  11494  mulcn2  11496  geoisum1c  11704  dvdsval2  11974  dvdsmodexp  11979  dvdsadd2b  12024  dvdsaddre2b  12025  dvdsmod  12046  oexpneg  12061  divalglemex  12106  divalg  12108  gcdass  12209  rplpwr  12221  rppwr  12222  nnminle  12229  lcmass  12280  coprmdvds2  12288  rpmulgcd2  12290  rpdvds  12294  cncongr2  12299  rpexp  12348  znege1  12373  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  coprimeprodsq2  12454  pythagtriplem3  12463  pythagtriplem4  12464  pcdvdsb  12516  pcbc  12547  ctinf  12674  nninfdc  12697  isnsgrp  13110  issubmnd  13146  nmzsubg  13418  ghmnsgima  13476  srg1zr  13621  ring1eq0  13682  mulgass2  13692  rhmdvdsr  13809  rmodislmod  13985  topssnei  14506  cnptopco  14566  cnconst2  14577  cnptoprest  14583  cnpdis  14586  upxp  14616  bldisj  14745  blgt0  14746  bl2in  14747  blss2ps  14750  blss2  14751  xblm  14761  blssps  14771  blss  14772  xmetresbl  14784  bdbl  14847  bdmopn  14848  metcnp3  14855  metcnp  14856  metcnp2  14857  dvfvalap  15025  dvcnp2cntop  15043  dvcn  15044  ply1term  15087  dvply1  15109  logdivlti  15225  ltexp2  15285  lgsfvalg  15354  lgsneg  15373  lgsdilem  15376  lgsdirprm  15383  lgsdir  15384  lgsdi  15386  lgsne0  15387  1dom1el  15745