Theorem simpl1l 1222

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  soisores  7326  tfisi  7850  funelss  8035  omopth2  8586  swrdsbslen  14618  swrdspsleq  14619  repswswrd  14738  ramub1lem1  16963  cntzsubrng  20455  cntzsubr  20496  lbspss  20837  maducoeval2  22362  cramer  22413  neiptopnei  22856  ptbasin  23301  basqtop  23435  tmdgsum  23819  ustuqtop1  23966  cxplea  26440  cxple2  26441  nosupbnd2lem1  27454  noinfbnd2lem1  27469  sltmul2  27862  ewlkle  29129  uspgr2wlkeq2  29171  clwwlkccat  29510  br8d  32106  isarchi2  32601  archiabllem2c  32611  cvmlift2lem10  34601  5segofs  35282  2llnjaN  38740  lvolnle3at  38756  paddasslem12  39005  paddasslem13  39006  atmod1i1m  39032  lhp2lt  39175  lhpexle2lem  39183  lhpmcvr3  39199  lhpat3  39220  ltrneq2  39322  trlnle  39360  trlval3  39361  trlval4  39362  cdleme0moN  39399  cdleme17b  39461  cdlemefrs29pre00  39569  cdlemefr27cl  39577  cdleme42ke  39659  cdleme42mgN  39662  cdleme46f2g2  39667  cdleme46f2g1  39668  cdleme50eq  39715  cdleme50trn3  39727  trlord  39743  cdlemg6c  39794  cdlemg11b  39816  cdlemg18a  39852  cdlemg42  39903  cdlemg46  39909  trljco  39914  tendococl  39946  cdlemj3  39997  tendotr  40004  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk53b  40130  cdlemk53  40131  cdlemk35u  40138  tendoex  40149  cdlemm10N  40292  dihopelvalcpre  40422  dihord6apre  40430  dihord5b  40433  dihglblem5apreN  40465  dihglblem2N  40468  dihmeetlem4preN  40480  dihmeetlem6  40483  dihmeetlem10N  40490  dihmeetlem11N  40491  dihmeetlem16N  40496  dihmeetlem17N  40497  dihmeetlem18N  40498  dihmeetlem19N  40499  dihmeetALTN  40501  dihlspsnat  40507  dvh3dim2  40622  dvh3dim3N  40623  jm2.25lem1  42039  jm2.26  42043  grur1cld  43293  limcperiod  44642  0ellimcdiv  44663  cncfshift  44888  cncfperiod  44893  icccncfext  44901  stoweidlem34  45048  fourierdlem48  45168  fourierdlem87  45207  sge0xaddlem2  45448  smflimsuplem7  45840  isomgrsym  46802  domnmsuppn0  47133  itscnhlinecirc02plem2  47556