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  7376  prarloclemarch2  7787  enq0tr  7802  distrlem4prl  7952  distrlem4pru  7953  ltaprg  7987  aptiprlemu  8008  lelttr  8415  ltletr  8416  readdcan  8468  addcan  8508  addcan2  8509  ltadd2  8749  ltmul1a  8922  ltmul1  8923  divmulassap  9028  divmulasscomap  9029  lemul1a  9191  xrlelttr  10219  xrltletr  10220  xaddass  10282  xleadd1a  10286  xltadd1  10289  xlesubadd  10296  ixxdisj  10316  icoshftf1o  10404  icodisj  10405  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  fztri3or  10454  ioom  10706  modqmuladdim  10819  modqmuladdnn0  10820  q2submod  10837  modqaddmulmod  10843  seqp1g  10918  exp3val  10993  ltexp2a  11043  exple1  11047  expnbnd  11116  expnlbnd2  11118  nn0ltexp2  11163  nn0leexp2  11164  mulsubdivbinom2ap  11165  expcan  11170  fiprsshashgt1  11274  hashtpgim  11313  hashtpg  11315  fun2dmnop0  11318  ccatass  11392  fzowrddc  11435  swrdclg  11438  ccatopth  11504  pfxccatin12lem2a  11515  maxleastb  11997  maxltsup  12001  xrltmaxsup  12042  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  addcn2  12095  mulcn2  12097  geoisum1c  12306  dvdsval2  12576  dvdsmodexp  12581  dvdsadd2b  12626  dvdsaddre2b  12627  dvdsmod  12648  oexpneg  12663  divalglemex  12708  divalg  12710  gcdass  12811  rplpwr  12823  rppwr  12824  nnminle  12831  lcmass  12882  coprmdvds2  12890  rpmulgcd2  12892  rpdvds  12896  cncongr2  12901  rpexp  12951  znege1  12977  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  coprimeprodsq2  13060  pythagtriplem3  13069  pythagtriplem4  13070  pcdvdsb  13122  pcbc  13153  ctinf  13373  nninfdc  13396  isnsgrp  13774  issubmnd  13808  nmzsubg  14066  ghmnsgima  14124  ring1eq0  14437  mulgass2  14447  rhmdvdsr  14566  rmodislmod  14772  issubassa  15097  topssnei  15354  cnptopco  15414  cnconst2  15425  cnptoprest  15431  cnpdis  15434  upxp  15464  bldisj  15593  blgt0  15594  bl2in  15595  blss2ps  15598  blss2  15599  xblm  15609  blssps  15619  blss  15620  xmetresbl  15632  bdbl  15695  bdmopn  15696  metcnp3  15703  metcnp  15704  metcnp2  15705  dvfvalap  15873  dvcnp2cntop  15891  dvcn  15892  ply1term  15935  dvply1  15957  logdivlti  16075  ltexp2  16138  pellexlem2  16191  bcmono  16265  lgsfvalg  16290  lgsneg  16309  lgsdilem  16312  lgsdirprm  16319  lgsdir  16320  lgsdi  16322  lgsne0  16323  clwwlknonex2e  16847