Theorem simpl2 1027

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

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

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 1006

This theorem is referenced by:  simpll2  1063  simprl2  1069  simp1l2  1117  simp2l2  1123  simp3l2  1129  3anandirs  1384  rspc3ev  2927  ifnetruedc  3649  tfisi  4685  brcogw  4899  oawordi  6637  nnmord  6685  nnmword  6686  1dom1el  6993  ac6sfi  7087  unsnfi  7111  unsnfidcel  7113  ordiso2  7234  prarloclemarch2  7639  enq0tr  7654  distrlem4prl  7804  distrlem4pru  7805  ltaprg  7839  aptiprlemu  7860  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  ltadd2  8599  ltmul1a  8771  ltmul1  8772  divmulassap  8875  divmulasscomap  8876  lemul1a  9038  xrlelttr  10041  xrltletr  10042  xaddass  10104  xleadd1a  10108  xltadd1  10111  xlesubadd  10118  ixxdisj  10138  icoshftf1o  10226  icodisj  10227  lincmb01cmp  10238  iccf1o  10239  fztri3or  10274  ioom  10521  modqmuladdim  10630  modqmuladdnn0  10631  q2submod  10648  modqaddmulmod  10654  seqp1g  10729  exp3val  10804  ltexp2a  10854  exple1  10858  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  nn0leexp2  10973  mulsubdivbinom2ap  10974  expcan  10979  fiprsshashgt1  11082  hashtpgim  11110  hashtpg  11112  fun2dmnop0  11115  ccatass  11189  fzowrddc  11232  swrdclg  11235  ccatopth  11301  pfxccatin12lem2a  11312  maxleastb  11792  maxltsup  11796  xrltmaxsup  11835  xrmaxltsup  11836  xrmaxaddlem  11838  xrmaxadd  11839  addcn2  11888  mulcn2  11890  geoisum1c  12099  dvdsval2  12369  dvdsmodexp  12374  dvdsadd2b  12419  dvdsaddre2b  12420  dvdsmod  12441  oexpneg  12456  divalglemex  12501  divalg  12503  gcdass  12604  rplpwr  12616  rppwr  12617  nnminle  12624  lcmass  12675  coprmdvds2  12683  rpmulgcd2  12685  rpdvds  12689  cncongr2  12694  rpexp  12743  znege1  12768  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  coprimeprodsq2  12849  pythagtriplem3  12858  pythagtriplem4  12859  pcdvdsb  12911  pcbc  12942  ctinf  13069  nninfdc  13092  isnsgrp  13507  issubmnd  13543  nmzsubg  13815  ghmnsgima  13873  srg1zr  14019  ring1eq0  14080  mulgass2  14090  rhmdvdsr  14208  rmodislmod  14384  topssnei  14905  cnptopco  14965  cnconst2  14976  cnptoprest  14982  cnpdis  14985  upxp  15015  bldisj  15144  blgt0  15145  bl2in  15146  blss2ps  15149  blss2  15150  xblm  15160  blssps  15170  blss  15171  xmetresbl  15183  bdbl  15246  bdmopn  15247  metcnp3  15254  metcnp  15255  metcnp2  15256  dvfvalap  15424  dvcnp2cntop  15442  dvcn  15443  ply1term  15486  dvply1  15508  logdivlti  15624  ltexp2  15684  lgsfvalg  15753  lgsneg  15772  lgsdilem  15775  lgsdirprm  15782  lgsdir  15783  lgsdi  15785  lgsne0  15786  clwwlknonex2e  16310