Theorem simpl1 995

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

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

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 975

This theorem is referenced by:  simpll1  1031  simprl1  1037  simp1l1  1085  simp2l1  1091  simp3l1  1097  3anandirs  1343  rspc3ev  2851  brcogw  4780  cocan1  5766  oawordi  6448  nnmord  6496  nnmword  6497  dif1en  6857  ac6sfi  6876  ordiso2  7012  difinfsn  7077  ctssdc  7090  enq0tr  7396  distrlem4prl  7546  distrlem4pru  7547  ltaprg  7581  aptiprlemu  7602  lelttr  8008  readdcan  8059  addcan  8099  addcan2  8100  ltadd2  8338  ltmul1a  8510  ltmul1  8511  divmulassap  8612  divmulasscomap  8613  lemul1a  8774  xrlelttr  9763  xleadd1a  9830  xlesubadd  9840  icoshftf1o  9948  lincmb01cmp  9960  iccf1o  9961  fztri3or  9995  fzofzim  10144  ioom  10217  modqmuladdim  10323  modqm1p1mod0  10331  q2submod  10341  modqaddmulmod  10347  ltexp2a  10528  exple1  10532  expnlbnd2  10601  nn0ltexp2  10644  nn0leexp2  10645  expcan  10650  fiprsshashgt1  10752  fimaxq  10762  maxleastb  11178  maxltsup  11182  xrltmaxsup  11220  xrmaxltsup  11221  xrmaxaddlem  11223  addcn2  11273  mulcn2  11275  dvdsmodexp  11757  dvdsadd2b  11802  dvdsmod  11822  oexpneg  11836  divalglemex  11881  divalg  11883  gcdass  11970  rplpwr  11982  rppwr  11983  nnwodc  11991  coprmdvds2  12047  rpmulgcd2  12049  qredeq  12050  rpdvds  12053  cncongr2  12058  rpexp  12107  znege1  12132  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  modprmn0modprm0  12210  coprimeprodsq2  12212  pythagtriplem3  12221  pcdvdsb  12273  pcgcd1  12281  qexpz  12304  pockthg  12309  ctinf  12385  nninfdc  12408  unbendc  12409  isnsgrp  12647  neiint  12939  topssnei  12956  iscnp4  13012  cnptopco  13016  cnconst2  13027  cnrest2  13030  cnptoprest  13033  cnpdis  13036  bldisj  13195  blgt0  13196  bl2in  13197  blss2ps  13200  blss2  13201  xblm  13211  blssps  13221  blss  13222  xmetresbl  13234  bdbl  13297  metcnp3  13305  metcnp2  13307  cncfmptc  13376  dvcnp2cntop  13457  dvcn  13458  logdivlti  13596  ltexp2  13654  lgsfcl2  13701  lgsdilem  13722  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgsne0  13733