Theorem simpl2 1028

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

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

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 1007

This theorem is referenced by:  simpll2  1064  simprl2  1070  simp1l2  1118  simp2l2  1124  simp3l2  1130  3anandirs  1385  rspc3ev  2938  ifnetruedc  3666  tfisi  4709  brcogw  4924  oawordi  6702  nnmord  6750  nnmword  6751  1dom1el  7060  mapunen  7104  ac6sfi  7155  unsnfi  7179  unsnfidcel  7181  ordiso2  7326  prarloclemarch2  7734  enq0tr  7749  distrlem4prl  7899  distrlem4pru  7900  ltaprg  7934  aptiprlemu  7955  lelttr  8362  ltletr  8363  readdcan  8413  addcan  8453  addcan2  8454  ltadd2  8693  ltmul1a  8865  ltmul1  8866  divmulassap  8969  divmulasscomap  8970  lemul1a  9132  xrlelttr  10139  xrltletr  10140  xaddass  10202  xleadd1a  10206  xltadd1  10209  xlesubadd  10216  ixxdisj  10236  icoshftf1o  10324  icodisj  10325  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  fztri3or  10373  ioom  10620  modqmuladdim  10729  modqmuladdnn0  10730  q2submod  10747  modqaddmulmod  10753  seqp1g  10828  exp3val  10903  ltexp2a  10953  exple1  10957  expnbnd  11025  expnlbnd2  11027  nn0ltexp2  11071  nn0leexp2  11072  mulsubdivbinom2ap  11073  expcan  11078  fiprsshashgt1  11182  hashtpgim  11217  hashtpg  11219  fun2dmnop0  11222  ccatass  11296  fzowrddc  11339  swrdclg  11342  ccatopth  11408  pfxccatin12lem2a  11419  maxleastb  11899  maxltsup  11903  xrltmaxsup  11942  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  addcn2  11995  mulcn2  11997  geoisum1c  12206  dvdsval2  12476  dvdsmodexp  12481  dvdsadd2b  12526  dvdsaddre2b  12527  dvdsmod  12548  oexpneg  12563  divalglemex  12608  divalg  12610  gcdass  12711  rplpwr  12723  rppwr  12724  nnminle  12731  lcmass  12782  coprmdvds2  12790  rpmulgcd2  12792  rpdvds  12796  cncongr2  12801  rpexp  12850  znege1  12875  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  coprimeprodsq2  12956  pythagtriplem3  12965  pythagtriplem4  12966  pcdvdsb  13018  pcbc  13049  ctinf  13181  nninfdc  13204  isnsgrp  13619  issubmnd  13655  nmzsubg  13927  ghmnsgima  13985  srg1zr  14131  ring1eq0  14192  mulgass2  14202  rhmdvdsr  14320  rmodislmod  14499  topssnei  15027  cnptopco  15087  cnconst2  15098  cnptoprest  15104  cnpdis  15107  upxp  15137  bldisj  15266  blgt0  15267  bl2in  15268  blss2ps  15271  blss2  15272  xblm  15282  blssps  15292  blss  15293  xmetresbl  15305  bdbl  15368  bdmopn  15369  metcnp3  15376  metcnp  15377  metcnp2  15378  dvfvalap  15546  dvcnp2cntop  15564  dvcn  15565  ply1term  15608  dvply1  15630  logdivlti  15746  ltexp2  15806  pellexlem2  15846  lgsfvalg  15878  lgsneg  15897  lgsdilem  15900  lgsdirprm  15907  lgsdir  15908  lgsdi  15910  lgsne0  15911  clwwlknonex2e  16435