Theorem simpl1l 1220

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7080  tfisi  7573  funelss  7746  omopth2  8210  swrdsbslen  14026  swrdspsleq  14027  repswswrd  14146  ramub1lem1  16362  cntzsubr  19568  lbspss  19854  maducoeval2  21249  cramer  21300  neiptopnei  21740  ptbasin  22185  basqtop  22319  tmdgsum  22703  ustuqtop1  22850  cxplea  25279  cxple2  25280  ewlkle  27387  uspgr2wlkeq2  27428  clwwlkccat  27768  br8d  30361  isarchi2  30814  archiabllem2c  30824  cvmlift2lem10  32559  nosupbnd2lem1  33215  5segofs  33467  2llnjaN  36717  lvolnle3at  36733  paddasslem12  36982  paddasslem13  36983  atmod1i1m  37009  lhp2lt  37152  lhpexle2lem  37160  lhpmcvr3  37176  lhpat3  37197  ltrneq2  37299  trlnle  37337  trlval3  37338  trlval4  37339  cdleme0moN  37376  cdleme17b  37438  cdlemefrs29pre00  37546  cdlemefr27cl  37554  cdleme42ke  37636  cdleme42mgN  37639  cdleme46f2g2  37644  cdleme46f2g1  37645  cdleme50eq  37692  cdleme50trn3  37704  trlord  37720  cdlemg6c  37771  cdlemg11b  37793  cdlemg18a  37829  cdlemg42  37880  cdlemg46  37886  trljco  37891  tendococl  37923  cdlemj3  37974  tendotr  37981  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk53b  38107  cdlemk53  38108  cdlemk35u  38115  tendoex  38126  cdlemm10N  38269  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihglblem5apreN  38442  dihglblem2N  38445  dihmeetlem4preN  38457  dihmeetlem6  38460  dihmeetlem10N  38467  dihmeetlem11N  38468  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem18N  38475  dihmeetlem19N  38476  dihmeetALTN  38478  dihlspsnat  38484  dvh3dim2  38599  dvh3dim3N  38600  jm2.25lem1  39615  jm2.26  39619  grur1cld  40588  limcperiod  41929  0ellimcdiv  41950  cncfshift  42177  cncfperiod  42182  icccncfext  42190  stoweidlem34  42339  fourierdlem48  42459  fourierdlem87  42498  sge0xaddlem2  42736  smflimsuplem7  43120  isomgrsym  44021  domnmsuppn0  44437  itscnhlinecirc02plem2  44790