Theorem simpl2 1001

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

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

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 980

This theorem is referenced by:  simpll2  1037  simprl2  1043  simp1l2  1091  simp2l2  1097  simp3l2  1103  3anandirs  1348  rspc3ev  2859  tfisi  4587  brcogw  4797  oawordi  6470  nnmord  6518  nnmword  6519  ac6sfi  6898  unsnfi  6918  unsnfidcel  6920  ordiso2  7034  prarloclemarch2  7418  enq0tr  7433  distrlem4prl  7583  distrlem4pru  7584  ltaprg  7618  aptiprlemu  7639  lelttr  8046  ltletr  8047  readdcan  8097  addcan  8137  addcan2  8138  ltadd2  8376  ltmul1a  8548  ltmul1  8549  divmulassap  8652  divmulasscomap  8653  lemul1a  8815  xrlelttr  9806  xrltletr  9807  xaddass  9869  xleadd1a  9873  xltadd1  9876  xlesubadd  9883  ixxdisj  9903  icoshftf1o  9991  icodisj  9992  lincmb01cmp  10003  iccf1o  10004  fztri3or  10039  ioom  10261  modqmuladdim  10367  modqmuladdnn0  10368  q2submod  10385  modqaddmulmod  10391  exp3val  10522  ltexp2a  10572  exple1  10576  expnbnd  10644  expnlbnd2  10646  nn0ltexp2  10689  nn0leexp2  10690  mulsubdivbinom2ap  10691  expcan  10696  fiprsshashgt1  10797  maxleastb  11223  maxltsup  11227  xrltmaxsup  11265  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  addcn2  11318  mulcn2  11320  geoisum1c  11528  dvdsval2  11797  dvdsmodexp  11802  dvdsadd2b  11847  dvdsaddre2b  11848  dvdsmod  11868  oexpneg  11882  divalglemex  11927  divalg  11929  gcdass  12016  rplpwr  12028  rppwr  12029  nnminle  12036  lcmass  12085  coprmdvds2  12093  rpmulgcd2  12095  rpdvds  12099  cncongr2  12104  rpexp  12153  znege1  12178  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  coprimeprodsq2  12258  pythagtriplem3  12267  pythagtriplem4  12268  pcdvdsb  12319  pcbc  12349  ctinf  12431  nninfdc  12454  isnsgrp  12812  issubmnd  12843  nmzsubg  13070  srg1zr  13170  ring1eq0  13225  mulgass2  13235  rmodislmod  13441  topssnei  13665  cnptopco  13725  cnconst2  13736  cnptoprest  13742  cnpdis  13745  upxp  13775  bldisj  13904  blgt0  13905  bl2in  13906  blss2ps  13909  blss2  13910  xblm  13920  blssps  13930  blss  13931  xmetresbl  13943  bdbl  14006  bdmopn  14007  metcnp3  14014  metcnp  14015  metcnp2  14016  dvfvalap  14153  dvcnp2cntop  14166  dvcn  14167  logdivlti  14305  ltexp2  14363  lgsfvalg  14409  lgsneg  14428  lgsdilem  14431  lgsdirprm  14438  lgsdir  14439  lgsdi  14441  lgsne0  14442