Theorem simpl1 1000

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

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

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 980

This theorem is referenced by:  simpll1  1036  simprl1  1042  simp1l1  1090  simp2l1  1096  simp3l1  1102  3anandirs  1348  rspc3ev  2858  brcogw  4796  cocan1  5787  oawordi  6469  nnmord  6517  nnmword  6518  dif1en  6878  ac6sfi  6897  ordiso2  7033  difinfsn  7098  ctssdc  7111  2omotaplemap  7255  enq0tr  7432  distrlem4prl  7582  distrlem4pru  7583  ltaprg  7617  aptiprlemu  7638  lelttr  8045  readdcan  8096  addcan  8136  addcan2  8137  ltadd2  8375  ltmul1a  8547  ltmul1  8548  divmulassap  8651  divmulasscomap  8652  lemul1a  8814  xrlelttr  9805  xleadd1a  9872  xlesubadd  9882  icoshftf1o  9990  lincmb01cmp  10002  iccf1o  10003  fztri3or  10038  fzofzim  10187  ioom  10260  modqmuladdim  10366  modqm1p1mod0  10374  q2submod  10384  modqaddmulmod  10390  ltexp2a  10571  exple1  10575  expnlbnd2  10645  nn0ltexp2  10688  nn0leexp2  10689  expcan  10695  fiprsshashgt1  10796  fimaxq  10806  maxleastb  11222  maxltsup  11226  xrltmaxsup  11264  xrmaxltsup  11265  xrmaxaddlem  11267  addcn2  11317  mulcn2  11319  dvdsmodexp  11801  dvdsadd2b  11846  dvdsmod  11867  oexpneg  11881  divalglemex  11926  divalg  11928  gcdass  12015  rplpwr  12027  rppwr  12028  nnwodc  12036  coprmdvds2  12092  rpmulgcd2  12094  qredeq  12095  rpdvds  12098  cncongr2  12103  rpexp  12152  znege1  12177  prmdiveq  12235  hashgcdlem  12237  odzdvds  12244  modprmn0modprm0  12255  coprimeprodsq2  12257  pythagtriplem3  12266  pcdvdsb  12318  pcgcd1  12326  qexpz  12349  pockthg  12354  ctinf  12430  nninfdc  12453  unbendc  12454  isnsgrp  12811  issubmnd  12842  ress0g  12843  mulgneg  13000  mulgdirlem  13012  subgmulg  13046  nmzsubg  13068  srg1zr  13168  ring1eq0  13223  mulgass2  13233  neiint  13581  topssnei  13598  iscnp4  13654  cnptopco  13658  cnconst2  13669  cnrest2  13672  cnptoprest  13675  cnpdis  13678  bldisj  13837  blgt0  13838  bl2in  13839  blss2ps  13842  blss2  13843  xblm  13853  blssps  13863  blss  13864  xmetresbl  13876  bdbl  13939  metcnp3  13947  metcnp2  13949  cncfmptc  14018  dvcnp2cntop  14099  dvcn  14100  logdivlti  14238  ltexp2  14296  lgsfcl2  14343  lgsdilem  14364  lgsdirprm  14371  lgsdir  14372  lgsdi  14374  lgsne0  14375