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  7358  tfisi  7894  funelss  8083  omopth2  8620  swrdsbslen  14842  swrdspsleq  14843  repswswrd  14963  ramub1lem1  17233  cntzsubrng  20849  cntzsubr  20888  lbspss  21387  maducoeval2  22985  cramer  23039  neiptopnei  23480  ptbasin  23926  basqtop  24060  tmdgsum  24444  ustuqtop1  24590  cxplea  27054  cxple2  27055  nosupbnd2lem1  28102  noinfbnd2lem1  28117  ltmuls2  28587  ewlkle  30216  uspgr2wlkeq2  30257  clwwlkccat  30611  br8d  33274  isarchi2  33816  archiabllem2c  33826  cvmlift2lem10  36244  5segofs  36949  2llnjaN  40815  lvolnle3at  40831  paddasslem12  41080  paddasslem13  41081  atmod1i1m  41107  lhp2lt  41250  lhpexle2lem  41258  lhpmcvr3  41274  lhpat3  41295  ltrneq2  41397  trlnle  41435  trlval3  41436  trlval4  41437  cdleme0moN  41474  cdleme17b  41536  cdlemefrs29pre00  41644  cdlemefr27cl  41652  cdleme42ke  41734  cdleme42mgN  41737  cdleme46f2g2  41742  cdleme46f2g1  41743  cdleme50eq  41790  cdleme50trn3  41802  trlord  41818  cdlemg6c  41869  cdlemg11b  41891  cdlemg18a  41927  cdlemg42  41978  cdlemg46  41984  trljco  41989  tendococl  42021  cdlemj3  42072  tendotr  42079  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk53b  42205  cdlemk53  42206  cdlemk35u  42213  tendoex  42224  cdlemm10N  42367  dihopelvalcpre  42497  dihord6apre  42505  dihord5b  42508  dihglblem5apreN  42540  dihglblem2N  42543  dihmeetlem4preN  42555  dihmeetlem6  42558  dihmeetlem10N  42565  dihmeetlem11N  42566  dihmeetlem16N  42571  dihmeetlem17N  42572  dihmeetlem18N  42573  dihmeetlem19N  42574  dihmeetALTN  42576  dihlspsnat  42582  dvh3dim2  42697  dvh3dim3N  42698  jm2.25lem1  44198  jm2.26  44202  grur1cld  45422  limcperiod  46845  0ellimcdiv  46864  cncfshift  47089  cncfperiod  47094  icccncfext  47102  stoweidlem34  47249  fourierdlem48  47369  fourierdlem87  47408  sge0xaddlem2  47649  smflimsuplem7  48041  domnmsuppn0  49686  itscnhlinecirc02plem2  50100