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  7335  tfisi  7870  funelss  8058  omopth2  8595  swrdsbslen  14818  swrdspsleq  14819  repswswrd  14939  ramub1lem1  17209  cntzsubrng  20824  cntzsubr  20863  lbspss  21362  maducoeval2  22960  cramer  23014  neiptopnei  23455  ptbasin  23901  basqtop  24035  tmdgsum  24419  ustuqtop1  24565  cxplea  27029  cxple2  27030  nosupbnd2lem1  28077  noinfbnd2lem1  28092  ltmuls2  28562  ewlkle  30191  uspgr2wlkeq2  30232  clwwlkccat  30586  br8d  33249  isarchi2  33792  archiabllem2c  33802  cvmlift2lem10  36163  5segofs  36863  2llnjaN  40716  lvolnle3at  40732  paddasslem12  40981  paddasslem13  40982  atmod1i1m  41008  lhp2lt  41151  lhpexle2lem  41159  lhpmcvr3  41175  lhpat3  41196  ltrneq2  41298  trlnle  41336  trlval3  41337  trlval4  41338  cdleme0moN  41375  cdleme17b  41437  cdlemefrs29pre00  41545  cdlemefr27cl  41553  cdleme42ke  41635  cdleme42mgN  41638  cdleme46f2g2  41643  cdleme46f2g1  41644  cdleme50eq  41691  cdleme50trn3  41703  trlord  41719  cdlemg6c  41770  cdlemg11b  41792  cdlemg18a  41828  cdlemg42  41879  cdlemg46  41885  trljco  41890  tendococl  41922  cdlemj3  41973  tendotr  41980  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk53b  42106  cdlemk53  42107  cdlemk35u  42114  tendoex  42125  cdlemm10N  42268  dihopelvalcpre  42398  dihord6apre  42406  dihord5b  42409  dihglblem5apreN  42441  dihglblem2N  42444  dihmeetlem4preN  42456  dihmeetlem6  42459  dihmeetlem10N  42466  dihmeetlem11N  42467  dihmeetlem16N  42472  dihmeetlem17N  42473  dihmeetlem18N  42474  dihmeetlem19N  42475  dihmeetALTN  42477  dihlspsnat  42483  dvh3dim2  42598  dvh3dim3N  42599  jm2.25lem1  44098  jm2.26  44102  grur1cld  45323  limcperiod  46733  0ellimcdiv  46752  cncfshift  46977  cncfperiod  46982  icccncfext  46990  stoweidlem34  47137  fourierdlem48  47257  fourierdlem87  47296  sge0xaddlem2  47537  smflimsuplem7  47929  domnmsuppn0  49574  itscnhlinecirc02plem2  49988