Theorem simpl2 1032

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

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

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 1011

This theorem is referenced by:  simpll2  1068  simprl2  1074  simp1l2  1122  simp2l2  1128  simp3l2  1134  3anandirs  1389  rspc3ev  2947  ifnetruedc  3681  tfisi  4729  brcogw  4944  oawordi  6732  nnmord  6780  nnmword  6781  1dom1el  7097  mapunen  7141  ac6sfi  7192  unsnfi  7216  unsnfidcel  7218  ordiso2  7365  prarloclemarch2  7776  enq0tr  7791  distrlem4prl  7941  distrlem4pru  7942  ltaprg  7976  aptiprlemu  7997  lelttr  8404  ltletr  8405  readdcan  8456  addcan  8496  addcan2  8497  ltadd2  8737  ltmul1a  8909  ltmul1  8910  divmulassap  9015  divmulasscomap  9016  lemul1a  9178  xrlelttr  10187  xrltletr  10188  xaddass  10250  xleadd1a  10254  xltadd1  10257  xlesubadd  10264  ixxdisj  10284  icoshftf1o  10372  icodisj  10373  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  fztri3or  10422  ioom  10673  modqmuladdim  10782  modqmuladdnn0  10783  q2submod  10800  modqaddmulmod  10806  seqp1g  10881  exp3val  10956  ltexp2a  11006  exple1  11010  expnbnd  11079  expnlbnd2  11081  nn0ltexp2  11125  nn0leexp2  11126  mulsubdivbinom2ap  11127  expcan  11132  fiprsshashgt1  11236  hashtpgim  11275  hashtpg  11277  fun2dmnop0  11280  ccatass  11354  fzowrddc  11397  swrdclg  11400  ccatopth  11466  pfxccatin12lem2a  11477  maxleastb  11958  maxltsup  11962  xrltmaxsup  12001  xrmaxltsup  12002  xrmaxaddlem  12004  xrmaxadd  12005  addcn2  12054  mulcn2  12056  geoisum1c  12265  dvdsval2  12535  dvdsmodexp  12540  dvdsadd2b  12585  dvdsaddre2b  12586  dvdsmod  12607  oexpneg  12622  divalglemex  12667  divalg  12669  gcdass  12770  rplpwr  12782  rppwr  12783  nnminle  12790  lcmass  12841  coprmdvds2  12849  rpmulgcd2  12851  rpdvds  12855  cncongr2  12860  rpexp  12909  znege1  12934  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  coprimeprodsq2  13015  pythagtriplem3  13024  pythagtriplem4  13025  pcdvdsb  13077  pcbc  13108  ctinf  13299  nninfdc  13322  isnsgrp  13698  issubmnd  13732  nmzsubg  13990  ghmnsgima  14048  ring1eq0  14326  mulgass2  14336  rhmdvdsr  14455  rmodislmod  14660  topssnei  15186  cnptopco  15246  cnconst2  15257  cnptoprest  15263  cnpdis  15266  upxp  15296  bldisj  15425  blgt0  15426  bl2in  15427  blss2ps  15430  blss2  15431  xblm  15441  blssps  15451  blss  15452  xmetresbl  15464  bdbl  15527  bdmopn  15528  metcnp3  15535  metcnp  15536  metcnp2  15537  dvfvalap  15705  dvcnp2cntop  15723  dvcn  15724  ply1term  15767  dvply1  15789  logdivlti  15905  ltexp2  15966  pellexlem2  16006  lgsfvalg  16038  lgsneg  16057  lgsdilem  16060  lgsdirprm  16067  lgsdir  16068  lgsdi  16070  lgsne0  16071  clwwlknonex2e  16595