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  4736  brcogw  4951  oawordi  6747  nnmord  6795  nnmword  6796  1dom1el  7113  mapunen  7157  ac6sfi  7208  unsnfi  7232  unsnfidcel  7234  ordiso2  7381  prarloclemarch2  7792  enq0tr  7807  distrlem4prl  7957  distrlem4pru  7958  ltaprg  7992  aptiprlemu  8013  lelttr  8420  ltletr  8421  readdcan  8473  addcan  8513  addcan2  8514  ltadd2  8754  ltmul1a  8927  ltmul1  8928  divmulassap  9033  divmulasscomap  9034  lemul1a  9196  xrlelttr  10224  xrltletr  10225  xaddass  10287  xleadd1a  10291  xltadd1  10294  xlesubadd  10301  ixxdisj  10321  icoshftf1o  10409  icodisj  10410  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  fztri3or  10459  ioom  10711  modqmuladdim  10824  modqmuladdnn0  10825  q2submod  10842  modqaddmulmod  10848  seqp1g  10923  exp3val  10998  ltexp2a  11048  exple1  11052  expnbnd  11121  expnlbnd2  11123  nn0ltexp2  11168  nn0leexp2  11169  mulsubdivbinom2ap  11170  expcan  11175  fiprsshashgt1  11279  hashtpgim  11318  hashtpg  11320  fun2dmnop0  11323  ccatass  11397  fzowrddc  11440  swrdclg  11443  ccatopth  11509  pfxccatin12lem2a  11520  maxleastb  12002  maxltsup  12006  xrltmaxsup  12047  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  addcn2  12100  mulcn2  12102  geoisum1c  12311  dvdsval2  12581  dvdsmodexp  12586  dvdsadd2b  12631  dvdsaddre2b  12632  dvdsmod  12653  oexpneg  12668  divalglemex  12713  divalg  12715  gcdass  12816  rplpwr  12828  rppwr  12829  nnminle  12836  lcmass  12887  coprmdvds2  12895  rpmulgcd2  12897  rpdvds  12901  cncongr2  12906  rpexp  12956  znege1  12982  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  coprimeprodsq2  13065  pythagtriplem3  13074  pythagtriplem4  13075  pcdvdsb  13127  pcbc  13158  ctinf  13378  nninfdc  13401  isnsgrp  13779  issubmnd  13813  nmzsubg  14071  ghmnsgima  14129  ring1eq0  14459  mulgass2  14469  rhmdvdsr  14590  rmodislmod  14796  issubassa  15121  snifpsrbagfi  15168  topssnei  15405  cnptopco  15465  cnconst2  15476  cnptoprest  15482  cnpdis  15485  upxp  15515  bldisj  15644  blgt0  15645  bl2in  15646  blss2ps  15649  blss2  15650  xblm  15660  blssps  15670  blss  15671  xmetresbl  15683  bdbl  15746  bdmopn  15747  metcnp3  15754  metcnp  15755  metcnp2  15756  dvfvalap  15924  dvcnp2cntop  15942  dvcn  15943  ply1term  15986  dvply1  16008  logdivlti  16128  efnthr  16193  ltexp2  16194  pellexlem2  16247  bcmono  16321  lgsfvalg  16346  lgsneg  16365  lgsdilem  16368  lgsdirprm  16375  lgsdir  16376  lgsdi  16378  lgsne0  16379  clwwlknonex2e  16903