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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1186	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  7302  tfisi  7835  funelss  8026  omopth2  8548  swrdsbslen  14629  swrdspsleq  14630  repswswrd  14749  ramub1lem1  16997  cntzsubrng  20476  cntzsubr  20515  lbspss  20989  maducoeval2  22527  cramer  22578  neiptopnei  23019  ptbasin  23464  basqtop  23598  tmdgsum  23982  ustuqtop1  24129  cxplea  26605  cxple2  26606  nosupbnd2lem1  27627  noinfbnd2lem1  27642  sltmul2  28074  ewlkle  29533  uspgr2wlkeq2  29575  clwwlkccat  29919  br8d  32538  isarchi2  33139  archiabllem2c  33149  cvmlift2lem10  35299  5segofs  35994  2llnjaN  39560  lvolnle3at  39576  paddasslem12  39825  paddasslem13  39826  atmod1i1m  39852  lhp2lt  39995  lhpexle2lem  40003  lhpmcvr3  40019  lhpat3  40040  ltrneq2  40142  trlnle  40180  trlval3  40181  trlval4  40182  cdleme0moN  40219  cdleme17b  40281  cdlemefrs29pre00  40389  cdlemefr27cl  40397  cdleme42ke  40479  cdleme42mgN  40482  cdleme46f2g2  40487  cdleme46f2g1  40488  cdleme50eq  40535  cdleme50trn3  40547  trlord  40563  cdlemg6c  40614  cdlemg11b  40636  cdlemg18a  40672  cdlemg42  40723  cdlemg46  40729  trljco  40734  tendococl  40766  cdlemj3  40817  tendotr  40824  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53b  40950  cdlemk53  40951  cdlemk35u  40958  tendoex  40969  cdlemm10N  41112  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihglblem5apreN  41285  dihglblem2N  41288  dihmeetlem4preN  41300  dihmeetlem6  41303  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem18N  41318  dihmeetlem19N  41319  dihmeetALTN  41321  dihlspsnat  41327  dvh3dim2  41442  dvh3dim3N  41443  jm2.25lem1  42987  jm2.26  42991  grur1cld  44221  limcperiod  45626  0ellimcdiv  45647  cncfshift  45872  cncfperiod  45877  icccncfext  45885  stoweidlem34  46032  fourierdlem48  46152  fourierdlem87  46191  sge0xaddlem2  46432  smflimsuplem7  46824  domnmsuppn0  48357  itscnhlinecirc02plem2  48772