Theorem simpl1l 1221

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

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

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 1086

This theorem is referenced by:  soisores  7059  tfisi  7553  funelss  7728  omopth2  8193  swrdsbslen  14017  swrdspsleq  14018  repswswrd  14137  ramub1lem1  16352  cntzsubr  19561  lbspss  19847  maducoeval2  21245  cramer  21296  neiptopnei  21737  ptbasin  22182  basqtop  22316  tmdgsum  22700  ustuqtop1  22847  cxplea  25287  cxple2  25288  ewlkle  27395  uspgr2wlkeq2  27436  clwwlkccat  27775  br8d  30374  isarchi2  30864  archiabllem2c  30874  cvmlift2lem10  32672  nosupbnd2lem1  33328  5segofs  33580  2llnjaN  36862  lvolnle3at  36878  paddasslem12  37127  paddasslem13  37128  atmod1i1m  37154  lhp2lt  37297  lhpexle2lem  37305  lhpmcvr3  37321  lhpat3  37342  ltrneq2  37444  trlnle  37482  trlval3  37483  trlval4  37484  cdleme0moN  37521  cdleme17b  37583  cdlemefrs29pre00  37691  cdlemefr27cl  37699  cdleme42ke  37781  cdleme42mgN  37784  cdleme46f2g2  37789  cdleme46f2g1  37790  cdleme50eq  37837  cdleme50trn3  37849  trlord  37865  cdlemg6c  37916  cdlemg11b  37938  cdlemg18a  37974  cdlemg42  38025  cdlemg46  38031  trljco  38036  tendococl  38068  cdlemj3  38119  tendotr  38126  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk53b  38252  cdlemk53  38253  cdlemk35u  38260  tendoex  38271  cdlemm10N  38414  dihopelvalcpre  38544  dihord6apre  38552  dihord5b  38555  dihglblem5apreN  38587  dihglblem2N  38590  dihmeetlem4preN  38602  dihmeetlem6  38605  dihmeetlem10N  38612  dihmeetlem11N  38613  dihmeetlem16N  38618  dihmeetlem17N  38619  dihmeetlem18N  38620  dihmeetlem19N  38621  dihmeetALTN  38623  dihlspsnat  38629  dvh3dim2  38744  dvh3dim3N  38745  jm2.25lem1  39939  jm2.26  39943  grur1cld  40940  limcperiod  42270  0ellimcdiv  42291  cncfshift  42516  cncfperiod  42521  icccncfext  42529  stoweidlem34  42676  fourierdlem48  42796  fourierdlem87  42835  sge0xaddlem2  43073  smflimsuplem7  43457  isomgrsym  44354  domnmsuppn0  44771  itscnhlinecirc02plem2  45197