Theorem simpl1 1026

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

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

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 1006

This theorem is referenced by:  simpll1  1062  simprl1  1068  simp1l1  1116  simp2l1  1122  simp3l1  1128  3anandirs  1384  rspc3ev  2927  brcogw  4899  cocan1  5928  oawordi  6637  nnmord  6685  nnmword  6686  dif1en  7068  ac6sfi  7087  ordiso2  7234  difinfsn  7299  ctssdc  7312  2omotaplemap  7476  enq0tr  7654  distrlem4prl  7804  distrlem4pru  7805  ltaprg  7839  aptiprlemu  7860  lelttr  8268  readdcan  8319  addcan  8359  addcan2  8360  ltadd2  8599  ltmul1a  8771  ltmul1  8772  divmulassap  8875  divmulasscomap  8876  lemul1a  9038  xrlelttr  10041  xleadd1a  10108  xlesubadd  10118  icoshftf1o  10226  lincmb01cmp  10238  iccf1o  10239  fztri3or  10274  nn0p1elfzo  10422  fzofzim  10428  ioom  10521  modqmuladdim  10630  modqm1p1mod0  10638  q2submod  10648  modqaddmulmod  10654  ltexp2a  10854  exple1  10858  expnlbnd2  10928  nn0ltexp2  10972  nn0leexp2  10973  expcan  10979  fiprsshashgt1  11082  fimaxq  11092  hashtpgim  11110  hashtpg  11112  fun2dmnop0  11115  ccatass  11189  swrdlen  11237  swrdfv  11238  swrdswrdlem  11289  ccatopth  11301  maxleastb  11792  maxltsup  11796  xrltmaxsup  11835  xrmaxltsup  11836  xrmaxaddlem  11838  addcn2  11888  mulcn2  11890  dvdsmodexp  12374  dvdsadd2b  12419  dvdsmod  12441  oexpneg  12456  divalglemex  12501  divalg  12503  gcdass  12604  rplpwr  12616  rppwr  12617  nnwodc  12625  coprmdvds2  12683  rpmulgcd2  12685  qredeq  12686  rpdvds  12689  cncongr2  12694  rpexp  12743  znege1  12768  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  modprmn0modprm0  12847  coprimeprodsq2  12849  pythagtriplem3  12858  pcdvdsb  12911  pcgcd1  12919  qexpz  12943  pockthg  12948  ctinf  13069  nninfdc  13092  unbendc  13093  isnsgrp  13507  issubmnd  13543  ress0g  13544  mulgneg  13745  mulgdirlem  13758  submmulg  13771  subgmulg  13793  nmzsubg  13815  ghmmulg  13861  srg1zr  14019  ring1eq0  14080  mulgass2  14090  rhmdvdsr  14208  rmodislmodlem  14383  rmodislmod  14384  lssintclm  14417  rnglidlrng  14531  2idlcpblrng  14556  neiint  14888  topssnei  14905  iscnp4  14961  cnptopco  14965  cnconst2  14976  cnrest2  14979  cnptoprest  14982  cnpdis  14985  bldisj  15144  blgt0  15145  bl2in  15146  blss2ps  15149  blss2  15150  xblm  15160  blssps  15170  blss  15171  xmetresbl  15183  bdbl  15246  metcnp3  15254  metcnp2  15256  cncfmptc  15339  dvcnp2cntop  15442  dvcn  15443  logdivlti  15624  ltexp2  15684  lgsfcl2  15754  lgsdilem  15775  lgsdirprm  15782  lgsdir  15783  lgsdi  15785  lgsne0  15786  incistruhgr  15960  clwwlkext2edg  16292  clwwlknonex2e  16310