Theorem simpl1l 1241

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl1l	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l

Step	Hyp	Ref	Expression
1		simpll 778	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1202	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  soisores  7315  tfisi  7843  funelss  8032  omopth2  8557  swrdsbslen  14692  swrdspsleq  14693  repswswrd  14811  ramub1lem1  17076  cntzsubrng  20643  cntzsubr  20682  lbspss  21172  maducoeval2  22758  cramer  22809  neiptopnei  23250  ptbasin  23695  basqtop  23829  tmdgsum  24213  ustuqtop1  24359  cxplea  26819  cxple2  26820  nosupbnd2lem1  27837  noinfbnd2lem1  27852  ltmuls2  28322  ewlkle  29864  uspgr2wlkeq2  29905  clwwlkccat  30250  br8d  32865  isarchi2  33418  archiabllem2c  33428  cvmlift2lem10  35675  5segofs  36369  2llnjaN  40202  lvolnle3at  40218  paddasslem12  40467  paddasslem13  40468  atmod1i1m  40494  lhp2lt  40637  lhpexle2lem  40645  lhpmcvr3  40661  lhpat3  40682  ltrneq2  40784  trlnle  40822  trlval3  40823  trlval4  40824  cdleme0moN  40861  cdleme17b  40923  cdlemefrs29pre00  41031  cdlemefr27cl  41039  cdleme42ke  41121  cdleme42mgN  41124  cdleme46f2g2  41129  cdleme46f2g1  41130  cdleme50eq  41177  cdleme50trn3  41189  trlord  41205  cdlemg6c  41256  cdlemg11b  41278  cdlemg18a  41314  cdlemg42  41365  cdlemg46  41371  trljco  41376  tendococl  41408  cdlemj3  41459  tendotr  41466  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53b  41592  cdlemk53  41593  cdlemk35u  41600  tendoex  41611  cdlemm10N  41754  dihopelvalcpre  41884  dihord6apre  41892  dihord5b  41895  dihglblem5apreN  41927  dihglblem2N  41930  dihmeetlem4preN  41942  dihmeetlem6  41945  dihmeetlem10N  41952  dihmeetlem11N  41953  dihmeetlem16N  41958  dihmeetlem17N  41959  dihmeetlem18N  41960  dihmeetlem19N  41961  dihmeetALTN  41963  dihlspsnat  41969  dvh3dim2  42084  dvh3dim3N  42085  jm2.25lem1  43587  jm2.26  43591  grur1cld  44820  limcperiod  46202  0ellimcdiv  46221  cncfshift  46446  cncfperiod  46451  icccncfext  46459  stoweidlem34  46606  fourierdlem48  46726  fourierdlem87  46765  sge0xaddlem2  47006  smflimsuplem7  47398  domnmsuppn0  49000  itscnhlinecirc02plem2  49414