Theorem simp-4l 790

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  naddssim  8640  marypha1lem  9365  acndom2  9996  ttukeylem6  10457  fpwwe2lem11  10585  swrdccatin1  14724  dfgcd2  16552  ramcl  17037  initoeu2lem1  18019  initoeu2  18021  chnind  18625  gsmsymgreqlem2  19443  dfod2  19576  pgpfi  19617  ghmcyg  19908  omndmul2  20145  suborng  20894  rhmpreimaidl  21316  psgndif  21623  mhpmulcl  22183  scmatmulcl  22547  cpmatmcllem  22747  neiptoptop  23160  cncnp  23309  subislly  23510  ptcnplem  23650  pthaus  23667  xkohaus  23682  kqreglem1  23770  cnextcn  24096  qustgplem  24150  trust  24258  utoptop  24263  restutopopn  24267  utop3cls  24280  utopreg  24281  isucn2  24307  met1stc  24550  metustsym  24584  metuel2  24594  xrge0tsms  24864  xmetdcn2  24867  nmoleub2lem2  25147  iscfil2  25297  iscfil3  25304  dvmptfsum  26006  dvlip2  26026  aannenlem1  26358  ulm2  26414  ulmuni  26421  mtestbdd  26434  efopn  26689  dchrptlem1  27294  pntpbnd  27618  pntibnd  27623  noetasuplem4  27766  f1otrg  29006  nbupgr  29480  upgriswlk  29776  usgr2pth  29899  clwwlkccatlem  30126  clwlkclwwlklem2a4  30134  cusconngr  30328  xrofsup  32908  ressprs  33094  gsummpt2d  33179  gsumfs2d  33191  xrge0tsmsd  33203  trsp2cyc  33253  isarchi3  33317  archirngz  33319  isarchiofld  33329  lmodslmd  33334  elrgspnlem4  33375  idlinsubrg  33563  rhmimaidl  33564  dimkerim  33868  sqsscirc1  34149  lmxrge0  34193  lmdvg  34194  esumrnmpt2  34309  esumfsup  34311  esumcvg  34327  esum2d  34334  ddemeas  34477  omssubadd  34541  satffunlem1lem1  35690  satffunlem2lem1  35692  btwnconn1lem13  36387  matunitlindflem1  38053  matunitlindflem2  38054  poimirlem29  38086  mblfinlem3  38096  mblfinlem4  38097  ftc1anclem7  38136  ftc1anc  38138  prdstotbnd  38231  ltrnid  40697  primrootscoprmpow  42654  posbezout  42655  primrootspoweq0  42661  aks6d1c6lem3  42727  unitscyglem3  42752  rencldnfilem  43335  pellex  43350  pellfundex  43401  dvdsacongtr  43499  naddcnff  43877  naddcnfid1  43882  oaun3lem1  43889  fnchoice  45547  climsuse  46122  addlimc  46160  0ellimcdiv  46161  climxrre  46262  xlimmnfvlem2  46345  xlimpnfvlem2  46349  icccncfext  46399  dvnprodlem3  46460  fourierdlem12  46631  fourierdlem34  46653  fourierdlem50  46668  fourierdlem80  46698  fourierdlem81  46699  fourierdlem87  46705  etransclem35  46781  sge0pr  46906  meaiuninc3v  46996  smfmullem3  47305  fsupdm  47354  finfdm  47358  cfsetsnfsetfo  47592  mogoldbb  48345  uzlidlring  48795  2zlidl  48800