Theorem simpl1 985

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

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

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

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

This theorem is referenced by:  simpll1  1021  simprl1  1027  simp1l1  1075  simp2l1  1081  simp3l1  1087  3anandirs  1327  rspc3ev  2810  brcogw  4716  cocan1  5696  oawordi  6373  nnmord  6421  nnmword  6422  dif1en  6781  ac6sfi  6800  ordiso2  6928  difinfsn  6993  ctssdc  7006  enq0tr  7266  distrlem4prl  7416  distrlem4pru  7417  ltaprg  7451  aptiprlemu  7472  lelttr  7876  readdcan  7926  addcan  7966  addcan2  7967  ltadd2  8205  ltmul1a  8377  ltmul1  8378  divmulassap  8479  divmulasscomap  8480  lemul1a  8640  xrlelttr  9619  xleadd1a  9686  xlesubadd  9696  icoshftf1o  9804  lincmb01cmp  9816  iccf1o  9817  fztri3or  9850  fzofzim  9996  ioom  10069  modqmuladdim  10171  modqm1p1mod0  10179  q2submod  10189  modqaddmulmod  10195  ltexp2a  10376  exple1  10380  expnlbnd2  10448  expcan  10494  fiprsshashgt1  10595  fimaxq  10605  maxleastb  11018  maxltsup  11022  xrltmaxsup  11058  xrmaxltsup  11059  xrmaxaddlem  11061  addcn2  11111  mulcn2  11113  dvdsadd2b  11576  dvdsmod  11596  oexpneg  11610  divalglemex  11655  divalg  11657  gcdass  11739  rplpwr  11751  rppwr  11752  coprmdvds2  11810  rpmulgcd2  11812  qredeq  11813  rpdvds  11816  cncongr2  11821  rpexp  11867  znege1  11892  hashgcdlem  11939  ctinf  11979  neiint  12353  topssnei  12370  iscnp4  12426  cnptopco  12430  cnconst2  12441  cnrest2  12444  cnptoprest  12447  cnpdis  12450  bldisj  12609  blgt0  12610  bl2in  12611  blss2ps  12614  blss2  12615  xblm  12625  blssps  12635  blss  12636  xmetresbl  12648  bdbl  12711  metcnp3  12719  metcnp2  12721  cncfmptc  12790  dvcnp2cntop  12871  dvcn  12872  logdivlti  13010