Theorem simp-4l 795

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4l	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad4antr 745	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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

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

This theorem is used by:  naddssim  8723  marypha1lem  9452  acndom2  10160  ttukeylem6  10619  fpwwe2lem11  10753  swrdccatin1  14902  dfgcd2  16748  ramcl  17236  initoeu2lem1  18218  initoeu2  18220  chnind  18824  gsmsymgreqlem2  19675  dfod2  19808  pgpfi  19849  ghmcyg  20140  omndmul2  20377  suborng  21163  rhmpreimaidl  21601  psgndif  21938  mhpmulcl  22500  scmatmulcl  22863  matunitlindflem1  23024  matunitlindflem2  23025  cpmatmcllem  23066  neiptoptop  23479  cncnp  23628  subislly  23830  ptcnplem  23970  pthaus  23987  xkohaus  24002  kqreglem1  24090  cnextcn  24416  qustgplem  24470  trust  24578  utoptop  24583  restutopopn  24587  utop3cls  24600  utopreg  24601  isucn2  24627  met1stc  24870  metustsym  24904  metuel2  24914  xrge0tsms  25184  xmetdcn2  25187  nmoleub2lem2  25467  iscfil2  25617  iscfil3  25624  dvmptfsum  26325  dvlip2  26345  aannenlem1  26685  ulm2  26742  ulmuni  26749  mtestbdd  26762  efopn  27016  dchrptlem1  27621  pntpbnd  27945  pntibnd  27950  noetasuplem4  28123  f1otrg  29478  nbupgr  29955  upgriswlk  30251  usgr2pth  30380  clwwlkccatlem  30610  clwlkclwwlklem2a4  30618  cusconngr  30822  xrofsup  33429  ressprs  33597  gsummpt2d  33680  gsumfs2d  33692  xrge0tsmsd  33704  trsp2cyc  33754  isarchi3  33818  archirngz  33820  isarchiofld  33830  lmodslmd  33835  elrgspnlem4  33876  idlinsubrg  34051  rhmimaidl  34052  dimkerim  34329  sqsscirc1  34610  lmxrge0  34654  lmdvg  34655  esumrnmpt2  34770  esumfsup  34772  esumcvg  34788  esum2d  34795  ddemeas  34939  satffunlem1lem1  36334  satffunlem2lem1  36336  btwnconn1lem13  37042  poimirlem29  38759  mblfinlem3  38769  mblfinlem4  38770  ftc1anclem7  38809  ftc1anc  38811  prdstotbnd  38920  ltrnid  41384  primrootscoprmpow  43341  posbezout  43342  primrootspoweq0  43348  aks6d1c6lem3  43414  unitscyglem3  43439  rencldnfilem  44020  pellex  44035  pellfundex  44086  dvdsacongtr  44184  naddcnff  44556  naddcnfid1  44561  oaun3lem1  44568  fnchoice  46251  climsuse  46825  addlimc  46863  0ellimcdiv  46864  climxrre  46965  xlimmnfvlem2  47048  xlimpnfvlem2  47052  icccncfext  47102  dvnprodlem3  47163  fourierdlem12  47334  fourierdlem34  47356  fourierdlem50  47371  fourierdlem80  47401  fourierdlem81  47402  fourierdlem87  47408  etransclem35  47484  sge0pr  47609  meaiuninc3v  47699  smfmullem3  48008  fsupdm  48057  finfdm  48061  cfsetsnfsetfo  48335  mogoldbb  49088  uzlidlring  49537  2zlidl  49542