Theorem simp-4l 782

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 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad4antr 732	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  naddssim  8697  marypha1lem  9445  acndom2  10068  ttukeylem6  10528  fpwwe2lem11  10655  swrdccatin1  14743  dfgcd2  16565  ramcl  17049  initoeu2lem1  18027  initoeu2  18029  gsmsymgreqlem2  19412  dfod2  19545  pgpfi  19586  ghmcyg  19877  rhmpreimaidl  21238  psgndif  21562  mhpmulcl  22087  scmatmulcl  22456  cpmatmcllem  22656  neiptoptop  23069  cncnp  23218  subislly  23419  ptcnplem  23559  pthaus  23576  xkohaus  23591  kqreglem1  23679  cnextcn  24005  qustgplem  24059  trust  24168  utoptop  24173  restutopopn  24177  utop3cls  24190  utopreg  24191  isucn2  24217  met1stc  24460  metustsym  24494  metuel2  24504  xrge0tsms  24774  xmetdcn2  24777  nmoleub2lem2  25067  iscfil2  25218  iscfil3  25225  dvmptfsum  25931  dvlip2  25952  aannenlem1  26288  ulm2  26346  ulmuni  26353  mtestbdd  26366  efopn  26619  dchrptlem1  27227  pntpbnd  27551  pntibnd  27556  noetasuplem4  27700  f1otrg  28850  nbupgr  29323  upgriswlk  29621  usgr2pth  29746  clwwlkccatlem  29970  clwlkclwwlklem2a4  29978  cusconngr  30172  xrofsup  32744  ressprs  32944  chnind  32991  gsummpt2d  33043  gsumfs2d  33049  xrge0tsmsd  33056  omndmul2  33080  trsp2cyc  33134  isarchi3  33185  archirngz  33187  lmodslmd  33201  elrgspnlem4  33240  suborng  33337  isarchiofld  33339  idlinsubrg  33446  rhmimaidl  33447  dimkerim  33667  sqsscirc1  33939  lmxrge0  33983  lmdvg  33984  esumrnmpt2  34099  esumfsup  34101  esumcvg  34117  esum2d  34124  ddemeas  34267  omssubadd  34332  satffunlem1lem1  35424  satffunlem2lem1  35426  btwnconn1lem13  36117  matunitlindflem1  37640  matunitlindflem2  37641  poimirlem29  37673  mblfinlem3  37683  mblfinlem4  37684  ftc1anclem7  37723  ftc1anc  37725  prdstotbnd  37818  ltrnid  40154  primrootscoprmpow  42112  posbezout  42113  primrootspoweq0  42119  aks6d1c6lem3  42185  unitscyglem3  42210  rencldnfilem  42843  pellex  42858  pellfundex  42909  dvdsacongtr  43008  naddcnff  43386  naddcnfid1  43391  oaun3lem1  43398  fnchoice  45053  climsuse  45637  addlimc  45677  0ellimcdiv  45678  climxrre  45779  xlimmnfvlem2  45862  xlimpnfvlem2  45866  icccncfext  45916  dvnprodlem3  45977  fourierdlem12  46148  fourierdlem34  46170  fourierdlem50  46185  fourierdlem80  46215  fourierdlem81  46216  fourierdlem87  46222  etransclem35  46298  sge0pr  46423  meaiuninc3v  46513  smfmullem3  46822  fsupdm  46871  finfdm  46875  cfsetsnfsetfo  47089  mogoldbb  47799  uzlidlring  48210  2zlidl  48215