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  2924  ifnetruedc  3646  tfisi  4679  brcogw  4891  oawordi  6623  nnmord  6671  nnmword  6672  ac6sfi  7068  unsnfi  7092  unsnfidcel  7094  ordiso2  7213  prarloclemarch2  7617  enq0tr  7632  distrlem4prl  7782  distrlem4pru  7783  ltaprg  7817  aptiprlemu  7838  lelttr  8246  ltletr  8247  readdcan  8297  addcan  8337  addcan2  8338  ltadd2  8577  ltmul1a  8749  ltmul1  8750  divmulassap  8853  divmulasscomap  8854  lemul1a  9016  xrlelttr  10014  xrltletr  10015  xaddass  10077  xleadd1a  10081  xltadd1  10084  xlesubadd  10091  ixxdisj  10111  icoshftf1o  10199  icodisj  10200  lincmb01cmp  10211  iccf1o  10212  fztri3or  10247  ioom  10492  modqmuladdim  10601  modqmuladdnn0  10602  q2submod  10619  modqaddmulmod  10625  seqp1g  10700  exp3val  10775  ltexp2a  10825  exple1  10829  expnbnd  10897  expnlbnd2  10899  nn0ltexp2  10943  nn0leexp2  10944  mulsubdivbinom2ap  10945  expcan  10950  fiprsshashgt1  11052  fun2dmnop0  11082  ccatass  11156  fzowrddc  11194  swrdclg  11197  ccatopth  11263  pfxccatin12lem2a  11274  maxleastb  11740  maxltsup  11744  xrltmaxsup  11783  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  addcn2  11836  mulcn2  11838  geoisum1c  12046  dvdsval2  12316  dvdsmodexp  12321  dvdsadd2b  12366  dvdsaddre2b  12367  dvdsmod  12388  oexpneg  12403  divalglemex  12448  divalg  12450  gcdass  12551  rplpwr  12563  rppwr  12564  nnminle  12571  lcmass  12622  coprmdvds2  12630  rpmulgcd2  12632  rpdvds  12636  cncongr2  12641  rpexp  12690  znege1  12715  prmdiveq  12773  hashgcdlem  12775  odzdvds  12783  coprimeprodsq2  12796  pythagtriplem3  12805  pythagtriplem4  12806  pcdvdsb  12858  pcbc  12889  ctinf  13016  nninfdc  13039  isnsgrp  13454  issubmnd  13490  nmzsubg  13762  ghmnsgima  13820  srg1zr  13965  ring1eq0  14026  mulgass2  14036  rhmdvdsr  14154  rmodislmod  14330  topssnei  14851  cnptopco  14911  cnconst2  14922  cnptoprest  14928  cnpdis  14931  upxp  14961  bldisj  15090  blgt0  15091  bl2in  15092  blss2ps  15095  blss2  15096  xblm  15106  blssps  15116  blss  15117  xmetresbl  15129  bdbl  15192  bdmopn  15193  metcnp3  15200  metcnp  15201  metcnp2  15202  dvfvalap  15370  dvcnp2cntop  15388  dvcn  15389  ply1term  15432  dvply1  15454  logdivlti  15570  ltexp2  15630  lgsfvalg  15699  lgsneg  15718  lgsdilem  15721  lgsdirprm  15728  lgsdir  15729  lgsdi  15731  lgsne0  15732  1dom1el  16409