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  8681  marypha1lem  9403  acndom2  10057  ttukeylem6  10516  fpwwe2lem11  10644  swrdccatin1  14786  dfgcd2  16629  ramcl  17114  initoeu2lem1  18096  initoeu2  18098  chnind  18702  gsmsymgreqlem2  19526  dfod2  19659  pgpfi  19700  ghmcyg  19991  omndmul2  20228  suborng  21009  rhmpreimaidl  21446  psgndif  21782  mhpmulcl  22342  scmatmulcl  22705  cpmatmcllem  22905  neiptoptop  23318  cncnp  23467  subislly  23668  ptcnplem  23808  pthaus  23825  xkohaus  23840  kqreglem1  23928  cnextcn  24254  qustgplem  24308  trust  24416  utoptop  24421  restutopopn  24425  utop3cls  24438  utopreg  24439  isucn2  24465  met1stc  24708  metustsym  24742  metuel2  24752  xrge0tsms  25022  xmetdcn2  25025  nmoleub2lem2  25305  iscfil2  25455  iscfil3  25462  dvmptfsum  26164  dvlip2  26184  aannenlem1  26521  ulm2  26578  ulmuni  26585  mtestbdd  26598  efopn  26853  dchrptlem1  27458  pntpbnd  27782  pntibnd  27787  noetasuplem4  27930  f1otrg  29250  nbupgr  29724  upgriswlk  30020  usgr2pth  30143  clwwlkccatlem  30370  clwlkclwwlklem2a4  30378  cusconngr  30572  xrofsup  33142  ressprs  33310  gsummpt2d  33393  gsumfs2d  33405  xrge0tsmsd  33417  trsp2cyc  33467  isarchi3  33531  archirngz  33533  isarchiofld  33543  lmodslmd  33548  elrgspnlem4  33589  idlinsubrg  33763  rhmimaidl  33764  dimkerim  34041  sqsscirc1  34322  lmxrge0  34366  lmdvg  34367  esumrnmpt2  34482  esumfsup  34484  esumcvg  34500  esum2d  34507  ddemeas  34650  omssubadd  34714  satffunlem1lem1  35907  satffunlem2lem1  35909  btwnconn1lem13  36604  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem29  38333  mblfinlem3  38343  mblfinlem4  38344  ftc1anclem7  38383  ftc1anc  38385  prdstotbnd  38478  ltrnid  40942  primrootscoprmpow  42899  posbezout  42900  primrootspoweq0  42906  aks6d1c6lem3  42972  unitscyglem3  42997  rencldnfilem  43580  pellex  43595  pellfundex  43646  dvdsacongtr  43744  naddcnff  44122  naddcnfid1  44127  oaun3lem1  44134  fnchoice  45782  climsuse  46357  addlimc  46395  0ellimcdiv  46396  climxrre  46497  xlimmnfvlem2  46580  xlimpnfvlem2  46584  icccncfext  46634  dvnprodlem3  46695  fourierdlem12  46866  fourierdlem34  46888  fourierdlem50  46903  fourierdlem80  46933  fourierdlem81  46934  fourierdlem87  46940  etransclem35  47016  sge0pr  47141  meaiuninc3v  47231  smfmullem3  47540  fsupdm  47589  finfdm  47593  cfsetsnfsetfo  47830  mogoldbb  48583  uzlidlring  49033  2zlidl  49038