Theorem simpl2 1025

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

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

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 1004

This theorem is referenced by:  simpll2  1061  simprl2  1067  simp1l2  1115  simp2l2  1121  simp3l2  1127  3anandirs  1382  rspc3ev  2924  ifnetruedc  3646  tfisi  4678  brcogw  4890  oawordi  6613  nnmord  6661  nnmword  6662  ac6sfi  7056  unsnfi  7077  unsnfidcel  7079  ordiso2  7198  prarloclemarch2  7602  enq0tr  7617  distrlem4prl  7767  distrlem4pru  7768  ltaprg  7802  aptiprlemu  7823  lelttr  8231  ltletr  8232  readdcan  8282  addcan  8322  addcan2  8323  ltadd2  8562  ltmul1a  8734  ltmul1  8735  divmulassap  8838  divmulasscomap  8839  lemul1a  9001  xrlelttr  9998  xrltletr  9999  xaddass  10061  xleadd1a  10065  xltadd1  10068  xlesubadd  10075  ixxdisj  10095  icoshftf1o  10183  icodisj  10184  lincmb01cmp  10195  iccf1o  10196  fztri3or  10231  ioom  10475  modqmuladdim  10584  modqmuladdnn0  10585  q2submod  10602  modqaddmulmod  10608  seqp1g  10683  exp3val  10758  ltexp2a  10808  exple1  10812  expnbnd  10880  expnlbnd2  10882  nn0ltexp2  10926  nn0leexp2  10927  mulsubdivbinom2ap  10928  expcan  10933  fiprsshashgt1  11034  fun2dmnop0  11064  ccatass  11138  fzowrddc  11174  swrdclg  11177  ccatopth  11243  pfxccatin12lem2a  11254  maxleastb  11720  maxltsup  11724  xrltmaxsup  11763  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  addcn2  11816  mulcn2  11818  geoisum1c  12026  dvdsval2  12296  dvdsmodexp  12301  dvdsadd2b  12346  dvdsaddre2b  12347  dvdsmod  12368  oexpneg  12383  divalglemex  12428  divalg  12430  gcdass  12531  rplpwr  12543  rppwr  12544  nnminle  12551  lcmass  12602  coprmdvds2  12610  rpmulgcd2  12612  rpdvds  12616  cncongr2  12621  rpexp  12670  znege1  12695  prmdiveq  12753  hashgcdlem  12755  odzdvds  12763  coprimeprodsq2  12776  pythagtriplem3  12785  pythagtriplem4  12786  pcdvdsb  12838  pcbc  12869  ctinf  12996  nninfdc  13019  isnsgrp  13434  issubmnd  13470  nmzsubg  13742  ghmnsgima  13800  srg1zr  13945  ring1eq0  14006  mulgass2  14016  rhmdvdsr  14133  rmodislmod  14309  topssnei  14830  cnptopco  14890  cnconst2  14901  cnptoprest  14907  cnpdis  14910  upxp  14940  bldisj  15069  blgt0  15070  bl2in  15071  blss2ps  15074  blss2  15075  xblm  15085  blssps  15095  blss  15096  xmetresbl  15108  bdbl  15171  bdmopn  15172  metcnp3  15179  metcnp  15180  metcnp2  15181  dvfvalap  15349  dvcnp2cntop  15367  dvcn  15368  ply1term  15411  dvply1  15433  logdivlti  15549  ltexp2  15609  lgsfvalg  15678  lgsneg  15697  lgsdilem  15700  lgsdirprm  15707  lgsdir  15708  lgsdi  15710  lgsne0  15711  1dom1el  16312