Theorem simpl1 947

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl1	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 944	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	adantr 271	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  simpll1  983  simprl1  989  simp1l1  1037  simp2l1  1043  simp3l1  1049  3anandirs  1285  rspc3ev  2739  brcogw  4618  cocan1  5580  oawordi  6244  nnmord  6290  nnmword  6291  dif1en  6649  ac6sfi  6668  ordiso2  6782  enq0tr  7054  distrlem4prl  7204  distrlem4pru  7205  ltaprg  7239  aptiprlemu  7260  lelttr  7634  readdcan  7683  addcan  7723  addcan2  7724  ltadd2  7958  ltmul1a  8129  ltmul1  8130  divmulassap  8223  divmulasscomap  8224  lemul1a  8380  xrlelttr  9332  icoshftf1o  9469  lincmb01cmp  9481  iccf1o  9482  fztri3or  9514  fzofzim  9660  ioom  9733  modqmuladdim  9835  modqm1p1mod0  9843  q2submod  9853  modqaddmulmod  9859  ltexp2a  10068  exple1  10072  expnlbnd2  10140  expcan  10186  fiprsshashgt1  10286  fimaxq  10296  maxleastb  10708  maxltsup  10712  addcn2  10760  mulcn2  10762  dvdsadd2b  11182  dvdsmod  11202  oexpneg  11216  divalglemex  11261  divalg  11263  gcdass  11343  rplpwr  11355  rppwr  11356  coprmdvds2  11414  rpmulgcd2  11416  qredeq  11417  rpdvds  11420  cncongr2  11425  rpexp  11471  znege1  11495  hashgcdlem  11542