Theorem simpl2 1032

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll2  1068  simprl2  1074  simp1l2  1122  simp2l2  1128  simp3l2  1134  3anandirs  1389  rspc3ev  2947  ifnetruedc  3684  tfisi  4736  brcogw  4951  oawordi  6746  nnmord  6794  nnmword  6795  1dom1el  7111  mapunen  7155  ac6sfi  7206  unsnfi  7230  unsnfidcel  7232  ordiso2  7381  prarloclemarch2  7792  enq0tr  7807  distrlem4prl  7957  distrlem4pru  7958  ltaprg  7992  aptiprlemu  8013  lelttr  8420  ltletr  8421  readdcan  8473  addcan  8513  addcan2  8514  ltadd2  8754  ltmul1a  8927  ltmul1  8928  divmulassap  9033  divmulasscomap  9034  lemul1a  9196  xrlelttr  10225  xrltletr  10226  xaddass  10288  xleadd1a  10292  xltadd1  10295  xlesubadd  10302  ixxdisj  10322  icoshftf1o  10410  icodisj  10411  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  fztri3or  10460  ioom  10712  modqmuladdim  10825  modqmuladdnn0  10826  q2submod  10843  modqaddmulmod  10849  seqp1g  10924  exp3val  10999  ltexp2a  11049  exple1  11053  expnbnd  11122  expnlbnd2  11124  nn0ltexp2  11169  nn0leexp2  11170  mulsubdivbinom2ap  11171  expcan  11176  fiprsshashgt1  11280  hashtpgim  11319  hashtpg  11321  fun2dmnop0  11324  ccatass  11398  fzowrddc  11441  swrdclg  11444  ccatopth  11510  pfxccatin12lem2a  11521  maxleastb  12003  maxltsup  12007  xrltmaxsup  12048  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  addcn2  12101  mulcn2  12103  geoisum1c  12312  dvdsval2  12582  dvdsmodexp  12587  dvdsadd2b  12632  dvdsaddre2b  12633  dvdsmod  12654  oexpneg  12669  divalglemex  12714  divalg  12716  gcdass  12817  rplpwr  12829  rppwr  12830  nnminle  12837  lcmass  12888  coprmdvds2  12896  rpmulgcd2  12898  rpdvds  12902  cncongr2  12907  rpexp  12957  znege1  12983  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  coprimeprodsq2  13066  pythagtriplem3  13075  pythagtriplem4  13076  pcdvdsb  13128  pcbc  13159  ctinf  13379  nninfdc  13402  isnsgrp  13780  issubmnd  13814  nmzsubg  14072  ghmnsgima  14130  ring1eq0  14460  mulgass2  14470  rhmdvdsr  14591  rmodislmod  14797  issubassa  15122  topssnei  15388  cnptopco  15448  cnconst2  15459  cnptoprest  15465  cnpdis  15468  upxp  15498  bldisj  15627  blgt0  15628  bl2in  15629  blss2ps  15632  blss2  15633  xblm  15643  blssps  15653  blss  15654  xmetresbl  15666  bdbl  15729  bdmopn  15730  metcnp3  15737  metcnp  15738  metcnp2  15739  dvfvalap  15907  dvcnp2cntop  15925  dvcn  15926  ply1term  15969  dvply1  15991  logdivlti  16111  efnthr  16176  ltexp2  16177  pellexlem2  16230  bcmono  16304  lgsfvalg  16329  lgsneg  16348  lgsdilem  16351  lgsdirprm  16358  lgsdir  16359  lgsdi  16361  lgsne0  16362  clwwlknonex2e  16886