Theorem simpl1l 1223

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

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

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 1088

This theorem is referenced by:  soisores  7346  tfisi  7879  funelss  8070  omopth2  8620  swrdsbslen  14698  swrdspsleq  14699  repswswrd  14818  ramub1lem1  17059  cntzsubrng  20583  cntzsubr  20622  lbspss  21098  maducoeval2  22661  cramer  22712  neiptopnei  23155  ptbasin  23600  basqtop  23734  tmdgsum  24118  ustuqtop1  24265  cxplea  26752  cxple2  26753  nosupbnd2lem1  27774  noinfbnd2lem1  27789  sltmul2  28211  ewlkle  29637  uspgr2wlkeq2  29679  clwwlkccat  30018  br8d  32629  isarchi2  33174  archiabllem2c  33184  cvmlift2lem10  35296  5segofs  35987  2llnjaN  39548  lvolnle3at  39564  paddasslem12  39813  paddasslem13  39814  atmod1i1m  39840  lhp2lt  39983  lhpexle2lem  39991  lhpmcvr3  40007  lhpat3  40028  ltrneq2  40130  trlnle  40168  trlval3  40169  trlval4  40170  cdleme0moN  40207  cdleme17b  40269  cdlemefrs29pre00  40377  cdlemefr27cl  40385  cdleme42ke  40467  cdleme42mgN  40470  cdleme46f2g2  40475  cdleme46f2g1  40476  cdleme50eq  40523  cdleme50trn3  40535  trlord  40551  cdlemg6c  40602  cdlemg11b  40624  cdlemg18a  40660  cdlemg42  40711  cdlemg46  40717  trljco  40722  tendococl  40754  cdlemj3  40805  tendotr  40812  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53b  40938  cdlemk53  40939  cdlemk35u  40946  tendoex  40957  cdlemm10N  41100  dihopelvalcpre  41230  dihord6apre  41238  dihord5b  41241  dihglblem5apreN  41273  dihglblem2N  41276  dihmeetlem4preN  41288  dihmeetlem6  41291  dihmeetlem10N  41298  dihmeetlem11N  41299  dihmeetlem16N  41304  dihmeetlem17N  41305  dihmeetlem18N  41306  dihmeetlem19N  41307  dihmeetALTN  41309  dihlspsnat  41315  dvh3dim2  41430  dvh3dim3N  41431  jm2.25lem1  42986  jm2.26  42990  grur1cld  44227  limcperiod  45583  0ellimcdiv  45604  cncfshift  45829  cncfperiod  45834  icccncfext  45842  stoweidlem34  45989  fourierdlem48  46109  fourierdlem87  46148  sge0xaddlem2  46389  smflimsuplem7  46781  domnmsuppn0  48213  itscnhlinecirc02plem2  48632