Theorem simpl2 1028

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

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

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 1007

This theorem is referenced by:  simpll2  1064  simprl2  1070  simp1l2  1118  simp2l2  1124  simp3l2  1130  3anandirs  1385  rspc3ev  2928  ifnetruedc  3653  tfisi  4691  brcogw  4905  oawordi  6680  nnmord  6728  nnmword  6729  1dom1el  7036  ac6sfi  7130  unsnfi  7154  unsnfidcel  7156  ordiso2  7277  prarloclemarch2  7682  enq0tr  7697  distrlem4prl  7847  distrlem4pru  7848  ltaprg  7882  aptiprlemu  7903  lelttr  8310  ltletr  8311  readdcan  8361  addcan  8401  addcan2  8402  ltadd2  8641  ltmul1a  8813  ltmul1  8814  divmulassap  8917  divmulasscomap  8918  lemul1a  9080  xrlelttr  10085  xrltletr  10086  xaddass  10148  xleadd1a  10152  xltadd1  10155  xlesubadd  10162  ixxdisj  10182  icoshftf1o  10270  icodisj  10271  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  fztri3or  10319  ioom  10566  modqmuladdim  10675  modqmuladdnn0  10676  q2submod  10693  modqaddmulmod  10699  seqp1g  10774  exp3val  10849  ltexp2a  10899  exple1  10903  expnbnd  10971  expnlbnd2  10973  nn0ltexp2  11017  nn0leexp2  11018  mulsubdivbinom2ap  11019  expcan  11024  fiprsshashgt1  11127  hashtpgim  11155  hashtpg  11157  fun2dmnop0  11160  ccatass  11234  fzowrddc  11277  swrdclg  11280  ccatopth  11346  pfxccatin12lem2a  11357  maxleastb  11837  maxltsup  11841  xrltmaxsup  11880  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  addcn2  11933  mulcn2  11935  geoisum1c  12144  dvdsval2  12414  dvdsmodexp  12419  dvdsadd2b  12464  dvdsaddre2b  12465  dvdsmod  12486  oexpneg  12501  divalglemex  12546  divalg  12548  gcdass  12649  rplpwr  12661  rppwr  12662  nnminle  12669  lcmass  12720  coprmdvds2  12728  rpmulgcd2  12730  rpdvds  12734  cncongr2  12739  rpexp  12788  znege1  12813  prmdiveq  12871  hashgcdlem  12873  odzdvds  12881  coprimeprodsq2  12894  pythagtriplem3  12903  pythagtriplem4  12904  pcdvdsb  12956  pcbc  12987  ctinf  13114  nninfdc  13137  isnsgrp  13552  issubmnd  13588  nmzsubg  13860  ghmnsgima  13918  srg1zr  14064  ring1eq0  14125  mulgass2  14135  rhmdvdsr  14253  rmodislmod  14430  topssnei  14956  cnptopco  15016  cnconst2  15027  cnptoprest  15033  cnpdis  15036  upxp  15066  bldisj  15195  blgt0  15196  bl2in  15197  blss2ps  15200  blss2  15201  xblm  15211  blssps  15221  blss  15222  xmetresbl  15234  bdbl  15297  bdmopn  15298  metcnp3  15305  metcnp  15306  metcnp2  15307  dvfvalap  15475  dvcnp2cntop  15493  dvcn  15494  ply1term  15537  dvply1  15559  logdivlti  15675  ltexp2  15735  pellexlem2  15775  lgsfvalg  15807  lgsneg  15826  lgsdilem  15829  lgsdirprm  15836  lgsdir  15837  lgsdi  15839  lgsne0  15840  clwwlknonex2e  16364