Theorem simpl1 1031

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4951  cocan1  5996  oawordi  6747  nnmord  6795  nnmword  6796  mapunen  7157  dif1en  7189  ac6sfi  7208  ordiso2  7381  difinfsn  7446  ctssdc  7459  2omotaplemap  7629  enq0tr  7807  distrlem4prl  7957  distrlem4pru  7958  ltaprg  7992  aptiprlemu  8013  lelttr  8420  readdcan  8473  addcan  8513  addcan2  8514  ltadd2  8754  ltmul1a  8927  ltmul1  8928  divmulassap  9033  divmulasscomap  9034  lemul1a  9196  xrlelttr  10224  xleadd1a  10291  xlesubadd  10301  icoshftf1o  10409  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  fztri3or  10459  nn0p1elfzo  10610  fzofzim  10616  ioom  10711  modqmuladdim  10824  modqm1p1mod0  10832  q2submod  10842  modqaddmulmod  10848  ltexp2a  11048  exple1  11052  expnlbnd2  11123  nn0ltexp2  11168  nn0leexp2  11169  expcan  11175  fiprsshashgt1  11279  fimaxq  11291  hashtpgim  11318  hashtpg  11320  fun2dmnop0  11323  ccatass  11397  swrdlen  11445  swrdfv  11446  swrdswrdlem  11497  ccatopth  11509  maxleastb  12002  maxltsup  12006  xrltmaxsup  12047  xrmaxltsup  12048  xrmaxaddlem  12050  addcn2  12100  mulcn2  12102  dvdsmodexp  12586  dvdsadd2b  12631  dvdsmod  12653  oexpneg  12668  divalglemex  12713  divalg  12715  gcdass  12816  rplpwr  12828  rppwr  12829  nnwodc  12837  coprmdvds2  12895  rpmulgcd2  12897  qredeq  12898  rpdvds  12901  cncongr2  12906  rpexp  12956  znege1  12982  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  modprmn0modprm0  13063  coprimeprodsq2  13065  pythagtriplem3  13074  pcdvdsb  13127  pcgcd1  13135  qexpz  13159  pockthg  13164  ctinf  13378  nninfdc  13401  unbendc  13402  isnsgrp  13779  issubmnd  13813  ress0g  13814  mulgneg  14001  mulgdirlem  14014  submmulg  14027  subgmulg  14049  nmzsubg  14071  ghmmulg  14117  ring1eq0  14459  mulgass2  14469  rhmdvdsr  14590  rmodislmodlem  14795  rmodislmod  14796  lssintclm  14829  rnglidlrng  14943  2idlcpblrng  14968  issubassa  15121  snifpsrbagfi  15168  neiint  15388  topssnei  15405  iscnp4  15461  cnptopco  15465  cnconst2  15476  cnrest2  15479  cnptoprest  15482  cnpdis  15485  bldisj  15644  blgt0  15645  bl2in  15646  blss2ps  15649  blss2  15650  xblm  15660  blssps  15670  blss  15671  xmetresbl  15683  bdbl  15746  metcnp3  15754  metcnp2  15756  cncfmptc  15839  dvcnp2cntop  15942  dvcn  15943  logdivlti  16128  ltexp2  16194  pellexlem2  16247  bcmono  16321  lgsfcl2  16347  lgsdilem  16368  lgsdirprm  16375  lgsdir  16376  lgsdi  16378  lgsne0  16379  incistruhgr  16553  clwwlkext2edg  16885  clwwlknonex2e  16903