Theorem simpl1 941

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpll1  977  simprl1  983  simp1l1  1031  simp2l1  1037  simp3l1  1043  3anandirs  1279  rspc3ev  2717  brcogw  4522  cocan1  5447  oawordi  6072  nnmord  6113  nnmword  6114  dif1en  6364  ac6sfi  6379  ordiso2  6446  enq0tr  6624  distrlem4prl  6774  distrlem4pru  6775  ltaprg  6809  aptiprlemu  6830  lelttr  7199  readdcan  7248  addcan  7288  addcan2  7289  ltadd2  7523  ltmul1a  7691  ltmul1  7692  divmulassap  7783  divmulasscomap  7784  lemul1a  7936  xrlelttr  8876  icoshftf1o  9013  lincmb01cmp  9025  iccf1o  9026  fztri3or  9058  fzofzim  9197  ioom  9269  modqmuladdim  9369  modqm1p1mod0  9377  q2submod  9387  modqaddmulmod  9393  ltexp2a  9528  exple1  9532  expnlbnd2  9598  expcan  9644  maxleastb  10100  maxltsup  10104  addcn2  10149  mulcn2  10151  dvdsadd2b  10242  dvdsmod  10262  oexpneg  10276  divalglemex  10322  divalg  10324  gcdass  10404  rplpwr  10416  rppwr  10417  coprmdvds2  10475  rpmulgcd2  10477  qredeq  10478  rpdvds  10481  cncongr2  10486  rpexp  10532  znege1  10556