Theorem simp-4l 794

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 744	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  naddssim  8671  marypha1lem  9392  acndom2  10037  ttukeylem6  10497  fpwwe2lem11  10625  swrdccatin1  14761  dfgcd2  16603  ramcl  17088  initoeu2lem1  18070  initoeu2  18072  chnind  18676  gsmsymgreqlem2  19500  dfod2  19633  pgpfi  19674  ghmcyg  19965  omndmul2  20202  suborng  20958  rhmpreimaidl  21395  psgndif  21731  mhpmulcl  22291  scmatmulcl  22654  cpmatmcllem  22854  neiptoptop  23267  cncnp  23416  subislly  23617  ptcnplem  23757  pthaus  23774  xkohaus  23789  kqreglem1  23877  cnextcn  24203  qustgplem  24257  trust  24365  utoptop  24370  restutopopn  24374  utop3cls  24387  utopreg  24388  isucn2  24414  met1stc  24657  metustsym  24691  metuel2  24701  xrge0tsms  24971  xmetdcn2  24974  nmoleub2lem2  25254  iscfil2  25404  iscfil3  25411  dvmptfsum  26113  dvlip2  26133  aannenlem1  26468  ulm2  26524  ulmuni  26531  mtestbdd  26544  efopn  26799  dchrptlem1  27404  pntpbnd  27728  pntibnd  27733  noetasuplem4  27876  f1otrg  29186  nbupgr  29660  upgriswlk  29956  usgr2pth  30079  clwwlkccatlem  30306  clwlkclwwlklem2a4  30314  cusconngr  30508  xrofsup  33078  ressprs  33252  gsummpt2d  33335  gsumfs2d  33347  xrge0tsmsd  33359  trsp2cyc  33409  isarchi3  33473  archirngz  33475  isarchiofld  33485  lmodslmd  33490  elrgspnlem4  33531  idlinsubrg  33705  rhmimaidl  33706  dimkerim  33983  sqsscirc1  34264  lmxrge0  34308  lmdvg  34309  esumrnmpt2  34424  esumfsup  34426  esumcvg  34442  esum2d  34449  ddemeas  34592  omssubadd  34656  satffunlem1lem1  35848  satffunlem2lem1  35850  btwnconn1lem13  36545  matunitlindflem1  38211  matunitlindflem2  38212  poimirlem29  38244  mblfinlem3  38254  mblfinlem4  38255  ftc1anclem7  38294  ftc1anc  38296  prdstotbnd  38389  ltrnid  40855  primrootscoprmpow  42812  posbezout  42813  primrootspoweq0  42819  aks6d1c6lem3  42885  unitscyglem3  42910  rencldnfilem  43495  pellex  43510  pellfundex  43561  dvdsacongtr  43659  naddcnff  44037  naddcnfid1  44042  oaun3lem1  44049  fnchoice  45697  climsuse  46272  addlimc  46310  0ellimcdiv  46311  climxrre  46412  xlimmnfvlem2  46495  xlimpnfvlem2  46499  icccncfext  46549  dvnprodlem3  46610  fourierdlem12  46781  fourierdlem34  46803  fourierdlem50  46818  fourierdlem80  46848  fourierdlem81  46849  fourierdlem87  46855  etransclem35  46931  sge0pr  47056  meaiuninc3v  47146  smfmullem3  47455  fsupdm  47504  finfdm  47508  cfsetsnfsetfo  47742  mogoldbb  48495  uzlidlring  48945  2zlidl  48950