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  4949  cocan1  5993  oawordi  6742  nnmord  6790  nnmword  6791  mapunen  7151  dif1en  7183  ac6sfi  7202  ordiso2  7376  difinfsn  7441  ctssdc  7454  2omotaplemap  7624  enq0tr  7802  distrlem4prl  7952  distrlem4pru  7953  ltaprg  7987  aptiprlemu  8008  lelttr  8415  readdcan  8468  addcan  8508  addcan2  8509  ltadd2  8749  ltmul1a  8922  ltmul1  8923  divmulassap  9028  divmulasscomap  9029  lemul1a  9191  xrlelttr  10219  xleadd1a  10286  xlesubadd  10296  icoshftf1o  10404  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  fztri3or  10454  nn0p1elfzo  10605  fzofzim  10611  ioom  10706  modqmuladdim  10819  modqm1p1mod0  10827  q2submod  10837  modqaddmulmod  10843  ltexp2a  11043  exple1  11047  expnlbnd2  11118  nn0ltexp2  11163  nn0leexp2  11164  expcan  11170  fiprsshashgt1  11274  fimaxq  11286  hashtpgim  11313  hashtpg  11315  fun2dmnop0  11318  ccatass  11392  swrdlen  11440  swrdfv  11441  swrdswrdlem  11492  ccatopth  11504  maxleastb  11997  maxltsup  12001  xrltmaxsup  12042  xrmaxltsup  12043  xrmaxaddlem  12045  addcn2  12095  mulcn2  12097  dvdsmodexp  12581  dvdsadd2b  12626  dvdsmod  12648  oexpneg  12663  divalglemex  12708  divalg  12710  gcdass  12811  rplpwr  12823  rppwr  12824  nnwodc  12832  coprmdvds2  12890  rpmulgcd2  12892  qredeq  12893  rpdvds  12896  cncongr2  12901  rpexp  12951  znege1  12977  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  modprmn0modprm0  13058  coprimeprodsq2  13060  pythagtriplem3  13069  pcdvdsb  13122  pcgcd1  13130  qexpz  13154  pockthg  13159  ctinf  13373  nninfdc  13396  unbendc  13397  isnsgrp  13774  issubmnd  13808  ress0g  13809  mulgneg  13996  mulgdirlem  14009  submmulg  14022  subgmulg  14044  nmzsubg  14066  ghmmulg  14112  ring1eq0  14437  mulgass2  14447  rhmdvdsr  14566  rmodislmodlem  14771  rmodislmod  14772  lssintclm  14805  rnglidlrng  14919  2idlcpblrng  14944  issubassa  15097  neiint  15337  topssnei  15354  iscnp4  15410  cnptopco  15414  cnconst2  15425  cnrest2  15428  cnptoprest  15431  cnpdis  15434  bldisj  15593  blgt0  15594  bl2in  15595  blss2ps  15598  blss2  15599  xblm  15609  blssps  15619  blss  15620  xmetresbl  15632  bdbl  15695  metcnp3  15703  metcnp2  15705  cncfmptc  15788  dvcnp2cntop  15891  dvcn  15892  logdivlti  16075  ltexp2  16138  pellexlem2  16191  bcmono  16265  lgsfcl2  16291  lgsdilem  16312  lgsdirprm  16319  lgsdir  16320  lgsdi  16322  lgsne0  16323  incistruhgr  16497  clwwlkext2edg  16829  clwwlknonex2e  16847