Theorem simpl1l 1226

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 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1187	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soisores  7282  tfisi  7810  funelss  8000  omopth2  8519  swrdsbslen  14627  swrdspsleq  14628  repswswrd  14746  ramub1lem1  16997  cntzsubrng  20544  cntzsubr  20583  lbspss  21077  maducoeval2  22605  cramer  22656  neiptopnei  23097  ptbasin  23542  basqtop  23676  tmdgsum  24060  ustuqtop1  24206  cxplea  26660  cxple2  26661  nosupbnd2lem1  27679  noinfbnd2lem1  27694  ltmuls2  28163  ewlkle  29674  uspgr2wlkeq2  29715  clwwlkccat  30060  br8d  32681  isarchi2  33246  archiabllem2c  33256  cvmlift2lem10  35494  5segofs  36188  2llnjaN  40012  lvolnle3at  40028  paddasslem12  40277  paddasslem13  40278  atmod1i1m  40304  lhp2lt  40447  lhpexle2lem  40455  lhpmcvr3  40471  lhpat3  40492  ltrneq2  40594  trlnle  40632  trlval3  40633  trlval4  40634  cdleme0moN  40671  cdleme17b  40733  cdlemefrs29pre00  40841  cdlemefr27cl  40849  cdleme42ke  40931  cdleme42mgN  40934  cdleme46f2g2  40939  cdleme46f2g1  40940  cdleme50eq  40987  cdleme50trn3  40999  trlord  41015  cdlemg6c  41066  cdlemg11b  41088  cdlemg18a  41124  cdlemg42  41175  cdlemg46  41181  trljco  41186  tendococl  41218  cdlemj3  41269  tendotr  41276  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53b  41402  cdlemk53  41403  cdlemk35u  41410  tendoex  41421  cdlemm10N  41564  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihglblem5apreN  41737  dihglblem2N  41740  dihmeetlem4preN  41752  dihmeetlem6  41755  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem18N  41770  dihmeetlem19N  41771  dihmeetALTN  41773  dihlspsnat  41779  dvh3dim2  41894  dvh3dim3N  41895  jm2.25lem1  43426  jm2.26  43430  grur1cld  44659  limcperiod  46058  0ellimcdiv  46077  cncfshift  46302  cncfperiod  46307  icccncfext  46315  stoweidlem34  46462  fourierdlem48  46582  fourierdlem87  46621  sge0xaddlem2  46862  smflimsuplem7  47254  domnmsuppn0  48845  itscnhlinecirc02plem2  49259