Theorem simpl1 1026

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 1023	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	adantr 276	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

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  fun2dmnop0  11112  ccatass  11186  swrdlen  11234  swrdfv  11235  swrdswrdlem  11286  ccatopth  11298  maxleastb  11776  maxltsup  11780  xrltmaxsup  11819  xrmaxltsup  11820  xrmaxaddlem  11822  addcn2  11872  mulcn2  11874  dvdsmodexp  12358  dvdsadd2b  12403  dvdsmod  12425  oexpneg  12440  divalglemex  12485  divalg  12487  gcdass  12588  rplpwr  12600  rppwr  12601  nnwodc  12609  coprmdvds2  12667  rpmulgcd2  12669  qredeq  12670  rpdvds  12673  cncongr2  12678  rpexp  12727  znege1  12752  prmdiveq  12810  hashgcdlem  12812  odzdvds  12820  modprmn0modprm0  12831  coprimeprodsq2  12833  pythagtriplem3  12842  pcdvdsb  12895  pcgcd1  12903  qexpz  12927  pockthg  12932  ctinf  13053  nninfdc  13076  unbendc  13077  isnsgrp  13491  issubmnd  13527  ress0g  13528  mulgneg  13729  mulgdirlem  13742  submmulg  13755  subgmulg  13777  nmzsubg  13799  ghmmulg  13845  srg1zr  14003  ring1eq0  14064  mulgass2  14074  rhmdvdsr  14192  rmodislmodlem  14367  rmodislmod  14368  lssintclm  14401  rnglidlrng  14515  2idlcpblrng  14540  neiint  14872  topssnei  14889  iscnp4  14945  cnptopco  14949  cnconst2  14960  cnrest2  14963  cnptoprest  14966  cnpdis  14969  bldisj  15128  blgt0  15129  bl2in  15130  blss2ps  15133  blss2  15134  xblm  15144  blssps  15154  blss  15155  xmetresbl  15167  bdbl  15230  metcnp3  15238  metcnp2  15240  cncfmptc  15323  dvcnp2cntop  15426  dvcn  15427  logdivlti  15608  ltexp2  15668  lgsfcl2  15738  lgsdilem  15759  lgsdirprm  15766  lgsdir  15767  lgsdi  15769  lgsne0  15770  incistruhgr  15944  clwwlkext2edg  16276  clwwlknonex2e  16294