Theorem simpl1l 1243

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7327  tfisi  7859  funelss  8047  omopth2  8576  swrdsbslen  14794  swrdspsleq  14795  repswswrd  14915  ramub1lem1  17184  cntzsubrng  20799  cntzsubr  20838  lbspss  21337  maducoeval2  22935  cramer  22989  neiptopnei  23430  ptbasin  23876  basqtop  24010  tmdgsum  24394  ustuqtop1  24540  cxplea  27006  cxple2  27007  nosupbnd2lem1  28054  noinfbnd2lem1  28069  ltmuls2  28539  ewlkle  30168  uspgr2wlkeq2  30209  clwwlkccat  30563  br8d  33184  isarchi2  33728  archiabllem2c  33738  cvmlift2lem10  36046  5segofs  36741  2llnjaN  40591  lvolnle3at  40607  paddasslem12  40856  paddasslem13  40857  atmod1i1m  40883  lhp2lt  41026  lhpexle2lem  41034  lhpmcvr3  41050  lhpat3  41071  ltrneq2  41173  trlnle  41211  trlval3  41212  trlval4  41213  cdleme0moN  41250  cdleme17b  41312  cdlemefrs29pre00  41420  cdlemefr27cl  41428  cdleme42ke  41510  cdleme42mgN  41513  cdleme46f2g2  41518  cdleme46f2g1  41519  cdleme50eq  41566  cdleme50trn3  41578  trlord  41594  cdlemg6c  41645  cdlemg11b  41667  cdlemg18a  41703  cdlemg42  41754  cdlemg46  41760  trljco  41765  tendococl  41797  cdlemj3  41848  tendotr  41855  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk53b  41981  cdlemk53  41982  cdlemk35u  41989  tendoex  42000  cdlemm10N  42143  dihopelvalcpre  42273  dihord6apre  42281  dihord5b  42284  dihglblem5apreN  42316  dihglblem2N  42319  dihmeetlem4preN  42331  dihmeetlem6  42334  dihmeetlem10N  42341  dihmeetlem11N  42342  dihmeetlem16N  42347  dihmeetlem17N  42348  dihmeetlem18N  42349  dihmeetlem19N  42350  dihmeetALTN  42352  dihlspsnat  42358  dvh3dim2  42473  dvh3dim3N  42474  jm2.25lem1  43958  jm2.26  43962  grur1cld  45189  limcperiod  46584  0ellimcdiv  46603  cncfshift  46828  cncfperiod  46833  icccncfext  46841  stoweidlem34  46988  fourierdlem48  47108  fourierdlem87  47147  sge0xaddlem2  47388  smflimsuplem7  47780  domnmsuppn0  49425  itscnhlinecirc02plem2  49839