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  7332  tfisi  7859  funelss  8048  omopth2  8575  swrdsbslen  14738  swrdspsleq  14739  repswswrd  14859  ramub1lem1  17124  cntzsubrng  20735  cntzsubr  20774  lbspss  21272  maducoeval2  22868  cramer  22922  neiptopnei  23363  ptbasin  23809  basqtop  23943  tmdgsum  24327  ustuqtop1  24473  cxplea  26941  cxple2  26942  nosupbnd2lem1  27959  noinfbnd2lem1  27974  ltmuls2  28444  ewlkle  30073  uspgr2wlkeq2  30114  clwwlkccat  30468  br8d  33089  isarchi2  33633  archiabllem2c  33643  cvmlift2lem10  35899  5segofs  36594  2llnjaN  40447  lvolnle3at  40463  paddasslem12  40712  paddasslem13  40713  atmod1i1m  40739  lhp2lt  40882  lhpexle2lem  40890  lhpmcvr3  40906  lhpat3  40927  ltrneq2  41029  trlnle  41067  trlval3  41068  trlval4  41069  cdleme0moN  41106  cdleme17b  41168  cdlemefrs29pre00  41276  cdlemefr27cl  41284  cdleme42ke  41366  cdleme42mgN  41369  cdleme46f2g2  41374  cdleme46f2g1  41375  cdleme50eq  41422  cdleme50trn3  41434  trlord  41450  cdlemg6c  41501  cdlemg11b  41523  cdlemg18a  41559  cdlemg42  41610  cdlemg46  41616  trljco  41621  tendococl  41653  cdlemj3  41704  tendotr  41711  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53b  41837  cdlemk53  41838  cdlemk35u  41845  tendoex  41856  cdlemm10N  41999  dihopelvalcpre  42129  dihord6apre  42137  dihord5b  42140  dihglblem5apreN  42172  dihglblem2N  42175  dihmeetlem4preN  42187  dihmeetlem6  42190  dihmeetlem10N  42197  dihmeetlem11N  42198  dihmeetlem16N  42203  dihmeetlem17N  42204  dihmeetlem18N  42205  dihmeetlem19N  42206  dihmeetALTN  42208  dihlspsnat  42214  dvh3dim2  42329  dvh3dim3N  42330  jm2.25lem1  43847  jm2.26  43851  grur1cld  45078  limcperiod  46466  0ellimcdiv  46485  cncfshift  46710  cncfperiod  46715  icccncfext  46723  stoweidlem34  46870  fourierdlem48  46990  fourierdlem87  47029  sge0xaddlem2  47270  smflimsuplem7  47662  domnmsuppn0  49307  itscnhlinecirc02plem2  49721