Theorem simpl2 1004

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

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

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 983

This theorem is referenced by:  simpll2  1040  simprl2  1046  simp1l2  1094  simp2l2  1100  simp3l2  1106  3anandirs  1361  rspc3ev  2898  ifnetruedc  3618  tfisi  4643  brcogw  4855  oawordi  6568  nnmord  6616  nnmword  6617  ac6sfi  7010  unsnfi  7031  unsnfidcel  7033  ordiso2  7152  prarloclemarch2  7552  enq0tr  7567  distrlem4prl  7717  distrlem4pru  7718  ltaprg  7752  aptiprlemu  7773  lelttr  8181  ltletr  8182  readdcan  8232  addcan  8272  addcan2  8273  ltadd2  8512  ltmul1a  8684  ltmul1  8685  divmulassap  8788  divmulasscomap  8789  lemul1a  8951  xrlelttr  9948  xrltletr  9949  xaddass  10011  xleadd1a  10015  xltadd1  10018  xlesubadd  10025  ixxdisj  10045  icoshftf1o  10133  icodisj  10134  lincmb01cmp  10145  iccf1o  10146  fztri3or  10181  ioom  10425  modqmuladdim  10534  modqmuladdnn0  10535  q2submod  10552  modqaddmulmod  10558  seqp1g  10633  exp3val  10708  ltexp2a  10758  exple1  10762  expnbnd  10830  expnlbnd2  10832  nn0ltexp2  10876  nn0leexp2  10877  mulsubdivbinom2ap  10878  expcan  10883  fiprsshashgt1  10984  fun2dmnop0  11014  ccatass  11087  fzowrddc  11123  swrdclg  11126  ccatopth  11192  maxleastb  11600  maxltsup  11604  xrltmaxsup  11643  xrmaxltsup  11644  xrmaxaddlem  11646  xrmaxadd  11647  addcn2  11696  mulcn2  11698  geoisum1c  11906  dvdsval2  12176  dvdsmodexp  12181  dvdsadd2b  12226  dvdsaddre2b  12227  dvdsmod  12248  oexpneg  12263  divalglemex  12308  divalg  12310  gcdass  12411  rplpwr  12423  rppwr  12424  nnminle  12431  lcmass  12482  coprmdvds2  12490  rpmulgcd2  12492  rpdvds  12496  cncongr2  12501  rpexp  12550  znege1  12575  prmdiveq  12633  hashgcdlem  12635  odzdvds  12643  coprimeprodsq2  12656  pythagtriplem3  12665  pythagtriplem4  12666  pcdvdsb  12718  pcbc  12749  ctinf  12876  nninfdc  12899  isnsgrp  13313  issubmnd  13349  nmzsubg  13621  ghmnsgima  13679  srg1zr  13824  ring1eq0  13885  mulgass2  13895  rhmdvdsr  14012  rmodislmod  14188  topssnei  14709  cnptopco  14769  cnconst2  14780  cnptoprest  14786  cnpdis  14789  upxp  14819  bldisj  14948  blgt0  14949  bl2in  14950  blss2ps  14953  blss2  14954  xblm  14964  blssps  14974  blss  14975  xmetresbl  14987  bdbl  15050  bdmopn  15051  metcnp3  15058  metcnp  15059  metcnp2  15060  dvfvalap  15228  dvcnp2cntop  15246  dvcn  15247  ply1term  15290  dvply1  15312  logdivlti  15428  ltexp2  15488  lgsfvalg  15557  lgsneg  15576  lgsdilem  15579  lgsdirprm  15586  lgsdir  15587  lgsdi  15589  lgsne0  15590  umgrnloopvv  15785  1dom1el  16065