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  11779  maxltsup  11783  xrltmaxsup  11822  xrmaxltsup  11823  xrmaxaddlem  11825  xrmaxadd  11826  addcn2  11875  mulcn2  11877  geoisum1c  12086  dvdsval2  12356  dvdsmodexp  12361  dvdsadd2b  12406  dvdsaddre2b  12407  dvdsmod  12428  oexpneg  12443  divalglemex  12488  divalg  12490  gcdass  12591  rplpwr  12603  rppwr  12604  nnminle  12611  lcmass  12662  coprmdvds2  12670  rpmulgcd2  12672  rpdvds  12676  cncongr2  12681  rpexp  12730  znege1  12755  prmdiveq  12813  hashgcdlem  12815  odzdvds  12823  coprimeprodsq2  12836  pythagtriplem3  12845  pythagtriplem4  12846  pcdvdsb  12898  pcbc  12929  ctinf  13056  nninfdc  13079  isnsgrp  13494  issubmnd  13530  nmzsubg  13802  ghmnsgima  13860  srg1zr  14006  ring1eq0  14067  mulgass2  14077  rhmdvdsr  14195  rmodislmod  14371  topssnei  14892  cnptopco  14952  cnconst2  14963  cnptoprest  14969  cnpdis  14972  upxp  15002  bldisj  15131  blgt0  15132  bl2in  15133  blss2ps  15136  blss2  15137  xblm  15147  blssps  15157  blss  15158  xmetresbl  15170  bdbl  15233  bdmopn  15234  metcnp3  15241  metcnp  15242  metcnp2  15243  dvfvalap  15411  dvcnp2cntop  15429  dvcn  15430  ply1term  15473  dvply1  15495  logdivlti  15611  ltexp2  15671  lgsfvalg  15740  lgsneg  15759  lgsdilem  15762  lgsdirprm  15769  lgsdir  15770  lgsdi  15772  lgsne0  15773  clwwlknonex2e  16297