Theorem simpl1l 1225

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 1186	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 400  df-3an 1090

This theorem is referenced by:  soisores  7087  tfisi  7586  funelss  7764  omopth2  8234  swrdsbslen  14108  swrdspsleq  14109  repswswrd  14228  ramub1lem1  16455  cntzsubr  19680  lbspss  19966  maducoeval2  21384  cramer  21435  neiptopnei  21876  ptbasin  22321  basqtop  22455  tmdgsum  22839  ustuqtop1  22986  cxplea  25431  cxple2  25432  ewlkle  27539  uspgr2wlkeq2  27580  clwwlkccat  27919  br8d  30516  isarchi2  31008  archiabllem2c  31018  cvmlift2lem10  32837  nosupbnd2lem1  33551  noinfbnd2lem1  33566  5segofs  33938  2llnjaN  37192  lvolnle3at  37208  paddasslem12  37457  paddasslem13  37458  atmod1i1m  37484  lhp2lt  37627  lhpexle2lem  37635  lhpmcvr3  37651  lhpat3  37672  ltrneq2  37774  trlnle  37812  trlval3  37813  trlval4  37814  cdleme0moN  37851  cdleme17b  37913  cdlemefrs29pre00  38021  cdlemefr27cl  38029  cdleme42ke  38111  cdleme42mgN  38114  cdleme46f2g2  38119  cdleme46f2g1  38120  cdleme50eq  38167  cdleme50trn3  38179  trlord  38195  cdlemg6c  38246  cdlemg11b  38268  cdlemg18a  38304  cdlemg42  38355  cdlemg46  38361  trljco  38366  tendococl  38398  cdlemj3  38449  tendotr  38456  cdlemk35s-id  38564  cdlemk39s-id  38566  cdlemk53b  38582  cdlemk53  38583  cdlemk35u  38590  tendoex  38601  cdlemm10N  38744  dihopelvalcpre  38874  dihord6apre  38882  dihord5b  38885  dihglblem5apreN  38917  dihglblem2N  38920  dihmeetlem4preN  38932  dihmeetlem6  38935  dihmeetlem10N  38942  dihmeetlem11N  38943  dihmeetlem16N  38948  dihmeetlem17N  38949  dihmeetlem18N  38950  dihmeetlem19N  38951  dihmeetALTN  38953  dihlspsnat  38959  dvh3dim2  39074  dvh3dim3N  39075  jm2.25lem1  40376  jm2.26  40380  grur1cld  41376  limcperiod  42695  0ellimcdiv  42716  cncfshift  42941  cncfperiod  42946  icccncfext  42954  stoweidlem34  43101  fourierdlem48  43221  fourierdlem87  43260  sge0xaddlem2  43498  smflimsuplem7  43882  isomgrsym  44806  domnmsuppn0  45223  itscnhlinecirc02plem2  45647