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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll2  1068  simprl2  1074  simp1l2  1122  simp2l2  1128  simp3l2  1134  3anandirs  1389  rspc3ev  2947  ifnetruedc  3684  tfisi  4734  brcogw  4949  oawordi  6742  nnmord  6790  nnmword  6791  1dom1el  7107  mapunen  7151  ac6sfi  7202  unsnfi  7226  unsnfidcel  7228  ordiso2  7375  prarloclemarch2  7786  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  aptiprlemu  8007  lelttr  8414  ltletr  8415  readdcan  8466  addcan  8506  addcan2  8507  ltadd2  8747  ltmul1a  8919  ltmul1  8920  divmulassap  9025  divmulasscomap  9026  lemul1a  9188  xrlelttr  10208  xrltletr  10209  xaddass  10271  xleadd1a  10275  xltadd1  10278  xlesubadd  10285  ixxdisj  10305  icoshftf1o  10393  icodisj  10394  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  fztri3or  10443  ioom  10695  modqmuladdim  10804  modqmuladdnn0  10805  q2submod  10822  modqaddmulmod  10828  seqp1g  10903  exp3val  10978  ltexp2a  11028  exple1  11032  expnbnd  11101  expnlbnd2  11103  nn0ltexp2  11147  nn0leexp2  11148  mulsubdivbinom2ap  11149  expcan  11154  fiprsshashgt1  11258  hashtpgim  11297  hashtpg  11299  fun2dmnop0  11302  ccatass  11376  fzowrddc  11419  swrdclg  11422  ccatopth  11488  pfxccatin12lem2a  11499  maxleastb  11980  maxltsup  11984  xrltmaxsup  12023  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  addcn2  12076  mulcn2  12078  geoisum1c  12287  dvdsval2  12557  dvdsmodexp  12562  dvdsadd2b  12607  dvdsaddre2b  12608  dvdsmod  12629  oexpneg  12644  divalglemex  12689  divalg  12691  gcdass  12792  rplpwr  12804  rppwr  12805  nnminle  12812  lcmass  12863  coprmdvds2  12871  rpmulgcd2  12873  rpdvds  12877  cncongr2  12882  rpexp  12931  znege1  12956  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  coprimeprodsq2  13037  pythagtriplem3  13046  pythagtriplem4  13047  pcdvdsb  13099  pcbc  13130  ctinf  13321  nninfdc  13344  isnsgrp  13721  issubmnd  13755  nmzsubg  14013  ghmnsgima  14071  ring1eq0  14353  mulgass2  14363  rhmdvdsr  14482  rmodislmod  14688  issubassa  15013  topssnei  15263  cnptopco  15323  cnconst2  15334  cnptoprest  15340  cnpdis  15343  upxp  15373  bldisj  15502  blgt0  15503  bl2in  15504  blss2ps  15507  blss2  15508  xblm  15518  blssps  15528  blss  15529  xmetresbl  15541  bdbl  15604  bdmopn  15605  metcnp3  15612  metcnp  15613  metcnp2  15614  dvfvalap  15782  dvcnp2cntop  15800  dvcn  15801  ply1term  15844  dvply1  15866  logdivlti  15982  ltexp2  16043  pellexlem2  16092  lgsfvalg  16124  lgsneg  16143  lgsdilem  16146  lgsdirprm  16153  lgsdir  16154  lgsdi  16156  lgsne0  16157  clwwlknonex2e  16681