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  8677  marypha1lem  9406  acndom2  10060  ttukeylem6  10519  fpwwe2lem11  10653  swrdccatin1  14796  dfgcd2  16640  ramcl  17125  initoeu2lem1  18107  initoeu2  18109  chnind  18713  gsmsymgreqlem2  19559  dfod2  19692  pgpfi  19733  ghmcyg  20024  omndmul2  20261  suborng  21043  rhmpreimaidl  21480  psgndif  21816  mhpmulcl  22378  scmatmulcl  22741  matunitlindflem1  22902  matunitlindflem2  22903  cpmatmcllem  22944  neiptoptop  23357  cncnp  23506  subislly  23708  ptcnplem  23848  pthaus  23865  xkohaus  23880  kqreglem1  23968  cnextcn  24294  qustgplem  24348  trust  24456  utoptop  24461  restutopopn  24465  utop3cls  24478  utopreg  24479  isucn2  24505  met1stc  24748  metustsym  24782  metuel2  24792  xrge0tsms  25062  xmetdcn2  25065  nmoleub2lem2  25345  iscfil2  25495  iscfil3  25502  dvmptfsum  26204  dvlip2  26224  aannenlem1  26561  ulm2  26618  ulmuni  26625  mtestbdd  26638  efopn  26893  dchrptlem1  27498  pntpbnd  27822  pntibnd  27827  noetasuplem4  27970  f1otrg  29313  nbupgr  29790  upgriswlk  30086  usgr2pth  30215  clwwlkccatlem  30445  clwlkclwwlklem2a4  30453  cusconngr  30657  xrofsup  33225  ressprs  33393  gsummpt2d  33476  gsumfs2d  33488  xrge0tsmsd  33500  trsp2cyc  33550  isarchi3  33614  archirngz  33616  isarchiofld  33626  lmodslmd  33631  elrgspnlem4  33672  idlinsubrg  33846  rhmimaidl  33847  dimkerim  34124  sqsscirc1  34405  lmxrge0  34449  lmdvg  34450  esumrnmpt2  34565  esumfsup  34567  esumcvg  34583  esum2d  34590  ddemeas  34734  omssubadd  34798  satffunlem1lem1  35968  satffunlem2lem1  35970  btwnconn1lem13  36666  poimirlem29  38385  mblfinlem3  38395  mblfinlem4  38396  ftc1anclem7  38435  ftc1anc  38437  prdstotbnd  38531  ltrnid  40995  primrootscoprmpow  42952  posbezout  42953  primrootspoweq0  42959  aks6d1c6lem3  43025  unitscyglem3  43050  rencldnfilem  43648  pellex  43663  pellfundex  43714  dvdsacongtr  43812  naddcnff  44190  naddcnfid1  44195  oaun3lem1  44202  fnchoice  45850  climsuse  46425  addlimc  46463  0ellimcdiv  46464  climxrre  46565  xlimmnfvlem2  46648  xlimpnfvlem2  46652  icccncfext  46702  dvnprodlem3  46763  fourierdlem12  46934  fourierdlem34  46956  fourierdlem50  46971  fourierdlem80  47001  fourierdlem81  47002  fourierdlem87  47008  etransclem35  47084  sge0pr  47209  meaiuninc3v  47299  smfmullem3  47608  fsupdm  47657  finfdm  47661  cfsetsnfsetfo  47935  mogoldbb  48688  uzlidlring  49137  2zlidl  49142