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

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

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 1089

This theorem is referenced by:  soisores  7347  tfisi  7880  funelss  8072  omopth2  8622  swrdsbslen  14702  swrdspsleq  14703  repswswrd  14822  ramub1lem1  17064  cntzsubrng  20567  cntzsubr  20606  lbspss  21081  maducoeval2  22646  cramer  22697  neiptopnei  23140  ptbasin  23585  basqtop  23719  tmdgsum  24103  ustuqtop1  24250  cxplea  26738  cxple2  26739  nosupbnd2lem1  27760  noinfbnd2lem1  27775  sltmul2  28197  ewlkle  29623  uspgr2wlkeq2  29665  clwwlkccat  30009  br8d  32622  isarchi2  33192  archiabllem2c  33202  cvmlift2lem10  35317  5segofs  36007  2llnjaN  39568  lvolnle3at  39584  paddasslem12  39833  paddasslem13  39834  atmod1i1m  39860  lhp2lt  40003  lhpexle2lem  40011  lhpmcvr3  40027  lhpat3  40048  ltrneq2  40150  trlnle  40188  trlval3  40189  trlval4  40190  cdleme0moN  40227  cdleme17b  40289  cdlemefrs29pre00  40397  cdlemefr27cl  40405  cdleme42ke  40487  cdleme42mgN  40490  cdleme46f2g2  40495  cdleme46f2g1  40496  cdleme50eq  40543  cdleme50trn3  40555  trlord  40571  cdlemg6c  40622  cdlemg11b  40644  cdlemg18a  40680  cdlemg42  40731  cdlemg46  40737  trljco  40742  tendococl  40774  cdlemj3  40825  tendotr  40832  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53b  40958  cdlemk53  40959  cdlemk35u  40966  tendoex  40977  cdlemm10N  41120  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihglblem5apreN  41293  dihglblem2N  41296  dihmeetlem4preN  41308  dihmeetlem6  41311  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem16N  41324  dihmeetlem17N  41325  dihmeetlem18N  41326  dihmeetlem19N  41327  dihmeetALTN  41329  dihlspsnat  41335  dvh3dim2  41450  dvh3dim3N  41451  jm2.25lem1  43010  jm2.26  43014  grur1cld  44251  limcperiod  45643  0ellimcdiv  45664  cncfshift  45889  cncfperiod  45894  icccncfext  45902  stoweidlem34  46049  fourierdlem48  46169  fourierdlem87  46208  sge0xaddlem2  46449  smflimsuplem7  46841  domnmsuppn0  48285  itscnhlinecirc02plem2  48704