Theorem simpl1 984

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

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

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 964

This theorem is referenced by:  simpll1  1020  simprl1  1026  simp1l1  1074  simp2l1  1080  simp3l1  1086  3anandirs  1326  rspc3ev  2801  brcogw  4703  cocan1  5681  oawordi  6358  nnmord  6406  nnmword  6407  dif1en  6766  ac6sfi  6785  ordiso2  6913  difinfsn  6978  ctssdc  6991  enq0tr  7235  distrlem4prl  7385  distrlem4pru  7386  ltaprg  7420  aptiprlemu  7441  lelttr  7845  readdcan  7895  addcan  7935  addcan2  7936  ltadd2  8174  ltmul1a  8346  ltmul1  8347  divmulassap  8448  divmulasscomap  8449  lemul1a  8609  xrlelttr  9582  xleadd1a  9649  xlesubadd  9659  icoshftf1o  9767  lincmb01cmp  9779  iccf1o  9780  fztri3or  9812  fzofzim  9958  ioom  10031  modqmuladdim  10133  modqm1p1mod0  10141  q2submod  10151  modqaddmulmod  10157  ltexp2a  10338  exple1  10342  expnlbnd2  10410  expcan  10456  fiprsshashgt1  10556  fimaxq  10566  maxleastb  10979  maxltsup  10983  xrltmaxsup  11019  xrmaxltsup  11020  xrmaxaddlem  11022  addcn2  11072  mulcn2  11074  dvdsadd2b  11529  dvdsmod  11549  oexpneg  11563  divalglemex  11608  divalg  11610  gcdass  11692  rplpwr  11704  rppwr  11705  coprmdvds2  11763  rpmulgcd2  11765  qredeq  11766  rpdvds  11769  cncongr2  11774  rpexp  11820  znege1  11845  hashgcdlem  11892  ctinf  11932  neiint  12303  topssnei  12320  iscnp4  12376  cnptopco  12380  cnconst2  12391  cnrest2  12394  cnptoprest  12397  cnpdis  12400  bldisj  12559  blgt0  12560  bl2in  12561  blss2ps  12564  blss2  12565  xblm  12575  blssps  12585  blss  12586  xmetresbl  12598  bdbl  12661  metcnp3  12669  metcnp2  12671  cncfmptc  12740  dvcnp2cntop  12821  dvcn  12822