Theorem simpl2 1025

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

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 1004

This theorem is referenced by:  simpll2  1061  simprl2  1067  simp1l2  1115  simp2l2  1121  simp3l2  1127  3anandirs  1382  rspc3ev  2925  ifnetruedc  3647  tfisi  4683  brcogw  4897  oawordi  6632  nnmord  6680  nnmword  6681  1dom1el  6988  ac6sfi  7080  unsnfi  7104  unsnfidcel  7106  ordiso2  7225  prarloclemarch2  7629  enq0tr  7644  distrlem4prl  7794  distrlem4pru  7795  ltaprg  7829  aptiprlemu  7850  lelttr  8258  ltletr  8259  readdcan  8309  addcan  8349  addcan2  8350  ltadd2  8589  ltmul1a  8761  ltmul1  8762  divmulassap  8865  divmulasscomap  8866  lemul1a  9028  xrlelttr  10031  xrltletr  10032  xaddass  10094  xleadd1a  10098  xltadd1  10101  xlesubadd  10108  ixxdisj  10128  icoshftf1o  10216  icodisj  10217  lincmb01cmp  10228  iccf1o  10229  fztri3or  10264  ioom  10510  modqmuladdim  10619  modqmuladdnn0  10620  q2submod  10637  modqaddmulmod  10643  seqp1g  10718  exp3val  10793  ltexp2a  10843  exple1  10847  expnbnd  10915  expnlbnd2  10917  nn0ltexp2  10961  nn0leexp2  10962  mulsubdivbinom2ap  10963  expcan  10968  fiprsshashgt1  11071  fun2dmnop0  11101  ccatass  11175  fzowrddc  11218  swrdclg  11221  ccatopth  11287  pfxccatin12lem2a  11298  maxleastb  11765  maxltsup  11769  xrltmaxsup  11808  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  addcn2  11861  mulcn2  11863  geoisum1c  12071  dvdsval2  12341  dvdsmodexp  12346  dvdsadd2b  12391  dvdsaddre2b  12392  dvdsmod  12413  oexpneg  12428  divalglemex  12473  divalg  12475  gcdass  12576  rplpwr  12588  rppwr  12589  nnminle  12596  lcmass  12647  coprmdvds2  12655  rpmulgcd2  12657  rpdvds  12661  cncongr2  12666  rpexp  12715  znege1  12740  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  coprimeprodsq2  12821  pythagtriplem3  12830  pythagtriplem4  12831  pcdvdsb  12883  pcbc  12914  ctinf  13041  nninfdc  13064  isnsgrp  13479  issubmnd  13515  nmzsubg  13787  ghmnsgima  13845  srg1zr  13990  ring1eq0  14051  mulgass2  14061  rhmdvdsr  14179  rmodislmod  14355  topssnei  14876  cnptopco  14936  cnconst2  14947  cnptoprest  14953  cnpdis  14956  upxp  14986  bldisj  15115  blgt0  15116  bl2in  15117  blss2ps  15120  blss2  15121  xblm  15131  blssps  15141  blss  15142  xmetresbl  15154  bdbl  15217  bdmopn  15218  metcnp3  15225  metcnp  15226  metcnp2  15227  dvfvalap  15395  dvcnp2cntop  15413  dvcn  15414  ply1term  15457  dvply1  15479  logdivlti  15595  ltexp2  15655  lgsfvalg  15724  lgsneg  15743  lgsdilem  15746  lgsdirprm  15753  lgsdir  15754  lgsdi  15756  lgsne0  15757  clwwlknonex2e  16235