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  8467  addcan  8507  addcan2  8508  ltadd2  8748  ltmul1a  8921  ltmul1  8922  divmulassap  9027  divmulasscomap  9028  lemul1a  9190  xrlelttr  10218  xrltletr  10219  xaddass  10281  xleadd1a  10285  xltadd1  10288  xlesubadd  10295  ixxdisj  10315  icoshftf1o  10403  icodisj  10404  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  fztri3or  10453  ioom  10705  modqmuladdim  10817  modqmuladdnn0  10818  q2submod  10835  modqaddmulmod  10841  seqp1g  10916  exp3val  10991  ltexp2a  11041  exple1  11045  expnbnd  11114  expnlbnd2  11116  nn0ltexp2  11161  nn0leexp2  11162  mulsubdivbinom2ap  11163  expcan  11168  fiprsshashgt1  11272  hashtpgim  11311  hashtpg  11313  fun2dmnop0  11316  ccatass  11390  fzowrddc  11433  swrdclg  11436  ccatopth  11502  pfxccatin12lem2a  11513  maxleastb  11995  maxltsup  11999  xrltmaxsup  12039  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  addcn2  12092  mulcn2  12094  geoisum1c  12303  dvdsval2  12573  dvdsmodexp  12578  dvdsadd2b  12623  dvdsaddre2b  12624  dvdsmod  12645  oexpneg  12660  divalglemex  12705  divalg  12707  gcdass  12808  rplpwr  12820  rppwr  12821  nnminle  12828  lcmass  12879  coprmdvds2  12887  rpmulgcd2  12889  rpdvds  12893  cncongr2  12898  rpexp  12948  znege1  12974  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  coprimeprodsq2  13057  pythagtriplem3  13066  pythagtriplem4  13067  pcdvdsb  13119  pcbc  13150  ctinf  13370  nninfdc  13393  isnsgrp  13770  issubmnd  13804  nmzsubg  14062  ghmnsgima  14120  ring1eq0  14402  mulgass2  14412  rhmdvdsr  14531  rmodislmod  14737  issubassa  15062  topssnei  15312  cnptopco  15372  cnconst2  15383  cnptoprest  15389  cnpdis  15392  upxp  15422  bldisj  15551  blgt0  15552  bl2in  15553  blss2ps  15556  blss2  15557  xblm  15567  blssps  15577  blss  15578  xmetresbl  15590  bdbl  15653  bdmopn  15654  metcnp3  15661  metcnp  15662  metcnp2  15663  dvfvalap  15831  dvcnp2cntop  15849  dvcn  15850  ply1term  15893  dvply1  15915  logdivlti  16033  ltexp2  16096  pellexlem2  16149  bcmono  16202  lgsfvalg  16222  lgsneg  16241  lgsdilem  16244  lgsdirprm  16251  lgsdir  16252  lgsdi  16254  lgsne0  16255  clwwlknonex2e  16779