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  6746  nnmord  6794  nnmword  6795  mapunen  7155  dif1en  7187  ac6sfi  7206  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  10225  xleadd1a  10292  xlesubadd  10302  icoshftf1o  10410  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  fztri3or  10460  nn0p1elfzo  10611  fzofzim  10617  ioom  10712  modqmuladdim  10825  modqm1p1mod0  10833  q2submod  10843  modqaddmulmod  10849  ltexp2a  11049  exple1  11053  expnlbnd2  11124  nn0ltexp2  11169  nn0leexp2  11170  expcan  11176  fiprsshashgt1  11280  fimaxq  11292  hashtpgim  11319  hashtpg  11321  fun2dmnop0  11324  ccatass  11398  swrdlen  11446  swrdfv  11447  swrdswrdlem  11498  ccatopth  11510  maxleastb  12003  maxltsup  12007  xrltmaxsup  12048  xrmaxltsup  12049  xrmaxaddlem  12051  addcn2  12101  mulcn2  12103  dvdsmodexp  12587  dvdsadd2b  12632  dvdsmod  12654  oexpneg  12669  divalglemex  12714  divalg  12716  gcdass  12817  rplpwr  12829  rppwr  12830  nnwodc  12838  coprmdvds2  12896  rpmulgcd2  12898  qredeq  12899  rpdvds  12902  cncongr2  12907  rpexp  12957  znege1  12983  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  modprmn0modprm0  13064  coprimeprodsq2  13066  pythagtriplem3  13075  pcdvdsb  13128  pcgcd1  13136  qexpz  13160  pockthg  13165  ctinf  13379  nninfdc  13402  unbendc  13403  isnsgrp  13780  issubmnd  13814  ress0g  13815  mulgneg  14002  mulgdirlem  14015  submmulg  14028  subgmulg  14050  nmzsubg  14072  ghmmulg  14118  ring1eq0  14460  mulgass2  14470  rhmdvdsr  14591  rmodislmodlem  14796  rmodislmod  14797  lssintclm  14830  rnglidlrng  14944  2idlcpblrng  14969  issubassa  15122  neiint  15371  topssnei  15388  iscnp4  15444  cnptopco  15448  cnconst2  15459  cnrest2  15462  cnptoprest  15465  cnpdis  15468  bldisj  15627  blgt0  15628  bl2in  15629  blss2ps  15632  blss2  15633  xblm  15643  blssps  15653  blss  15654  xmetresbl  15666  bdbl  15729  metcnp3  15737  metcnp2  15739  cncfmptc  15822  dvcnp2cntop  15925  dvcn  15926  logdivlti  16111  ltexp2  16177  pellexlem2  16230  bcmono  16304  lgsfcl2  16330  lgsdilem  16351  lgsdirprm  16358  lgsdir  16359  lgsdi  16361  lgsne0  16362  incistruhgr  16536  clwwlkext2edg  16868  clwwlknonex2e  16886