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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

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 401

This theorem is used by:  naddssim  8670  marypha1lem  9391  acndom2  10045  ttukeylem6  10504  fpwwe2lem11  10632  swrdccatin1  14769  dfgcd2  16610  ramcl  17095  initoeu2lem1  18077  initoeu2  18079  chnind  18683  gsmsymgreqlem2  19507  dfod2  19640  pgpfi  19681  ghmcyg  19972  omndmul2  20209  suborng  20990  rhmpreimaidl  21427  psgndif  21763  mhpmulcl  22323  scmatmulcl  22686  cpmatmcllem  22886  neiptoptop  23299  cncnp  23448  subislly  23649  ptcnplem  23789  pthaus  23806  xkohaus  23821  kqreglem1  23909  cnextcn  24235  qustgplem  24289  trust  24397  utoptop  24402  restutopopn  24406  utop3cls  24419  utopreg  24420  isucn2  24446  met1stc  24689  metustsym  24723  metuel2  24733  xrge0tsms  25003  xmetdcn2  25006  nmoleub2lem2  25286  iscfil2  25436  iscfil3  25443  dvmptfsum  26145  dvlip2  26165  aannenlem1  26502  ulm2  26559  ulmuni  26566  mtestbdd  26579  efopn  26834  dchrptlem1  27439  pntpbnd  27763  pntibnd  27768  noetasuplem4  27911  f1otrg  29231  nbupgr  29705  upgriswlk  30001  usgr2pth  30124  clwwlkccatlem  30351  clwlkclwwlklem2a4  30359  cusconngr  30553  xrofsup  33123  ressprs  33295  gsummpt2d  33378  gsumfs2d  33390  xrge0tsmsd  33402  trsp2cyc  33452  isarchi3  33516  archirngz  33518  isarchiofld  33528  lmodslmd  33533  elrgspnlem4  33574  idlinsubrg  33748  rhmimaidl  33749  dimkerim  34026  sqsscirc1  34307  lmxrge0  34351  lmdvg  34352  esumrnmpt2  34467  esumfsup  34469  esumcvg  34485  esum2d  34492  ddemeas  34635  omssubadd  34699  satffunlem1lem1  35902  satffunlem2lem1  35904  btwnconn1lem13  36599  matunitlindflem1  38295  matunitlindflem2  38296  poimirlem29  38328  mblfinlem3  38338  mblfinlem4  38339  ftc1anclem7  38378  ftc1anc  38380  prdstotbnd  38473  ltrnid  40937  primrootscoprmpow  42894  posbezout  42895  primrootspoweq0  42901  aks6d1c6lem3  42967  unitscyglem3  42992  rencldnfilem  43575  pellex  43590  pellfundex  43641  dvdsacongtr  43739  naddcnff  44117  naddcnfid1  44122  oaun3lem1  44129  fnchoice  45777  climsuse  46352  addlimc  46390  0ellimcdiv  46391  climxrre  46492  xlimmnfvlem2  46575  xlimpnfvlem2  46579  icccncfext  46629  dvnprodlem3  46690  fourierdlem12  46861  fourierdlem34  46883  fourierdlem50  46898  fourierdlem80  46928  fourierdlem81  46929  fourierdlem87  46935  etransclem35  47011  sge0pr  47136  meaiuninc3v  47226  smfmullem3  47535  fsupdm  47584  finfdm  47588  cfsetsnfsetfo  47825  mogoldbb  48578  uzlidlring  49028  2zlidl  49033