Theorem simp-4l 783

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 733	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  8621  marypha1lem  9346  acndom2  9976  ttukeylem6  10436  fpwwe2lem11  10564  swrdccatin1  14687  dfgcd2  16515  ramcl  17000  initoeu2lem1  17981  initoeu2  17983  chnind  18587  gsmsymgreqlem2  19406  dfod2  19539  pgpfi  19580  ghmcyg  19871  omndmul2  20108  suborng  20853  rhmpreimaidl  21275  psgndif  21582  mhpmulcl  22115  scmatmulcl  22483  cpmatmcllem  22683  neiptoptop  23096  cncnp  23245  subislly  23446  ptcnplem  23586  pthaus  23603  xkohaus  23618  kqreglem1  23706  cnextcn  24032  qustgplem  24086  trust  24194  utoptop  24199  restutopopn  24203  utop3cls  24216  utopreg  24217  isucn2  24243  met1stc  24486  metustsym  24520  metuel2  24530  xrge0tsms  24800  xmetdcn2  24803  nmoleub2lem2  25083  iscfil2  25233  iscfil3  25240  dvmptfsum  25942  dvlip2  25962  aannenlem1  26294  ulm2  26350  ulmuni  26357  mtestbdd  26370  efopn  26622  dchrptlem1  27227  pntpbnd  27551  pntibnd  27556  noetasuplem4  27700  f1otrg  28939  nbupgr  29413  upgriswlk  29709  usgr2pth  29832  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  cusconngr  30261  xrofsup  32840  ressprs  33026  gsummpt2d  33110  gsumfs2d  33122  xrge0tsmsd  33134  trsp2cyc  33184  isarchi3  33248  archirngz  33250  isarchiofld  33260  lmodslmd  33265  elrgspnlem4  33306  idlinsubrg  33491  rhmimaidl  33492  dimkerim  33771  sqsscirc1  34052  lmxrge0  34096  lmdvg  34097  esumrnmpt2  34212  esumfsup  34214  esumcvg  34230  esum2d  34237  ddemeas  34380  omssubadd  34444  satffunlem1lem1  35584  satffunlem2lem1  35586  btwnconn1lem13  36281  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem29  37970  mblfinlem3  37980  mblfinlem4  37981  ftc1anclem7  38020  ftc1anc  38022  prdstotbnd  38115  ltrnid  40581  primrootscoprmpow  42538  posbezout  42539  primrootspoweq0  42545  aks6d1c6lem3  42611  unitscyglem3  42636  rencldnfilem  43248  pellex  43263  pellfundex  43314  dvdsacongtr  43412  naddcnff  43790  naddcnfid1  43795  oaun3lem1  43802  fnchoice  45460  climsuse  46038  addlimc  46076  0ellimcdiv  46077  climxrre  46178  xlimmnfvlem2  46261  xlimpnfvlem2  46265  icccncfext  46315  dvnprodlem3  46376  fourierdlem12  46547  fourierdlem34  46569  fourierdlem50  46584  fourierdlem80  46614  fourierdlem81  46615  fourierdlem87  46621  etransclem35  46697  sge0pr  46822  meaiuninc3v  46912  smfmullem3  47221  fsupdm  47270  finfdm  47274  cfsetsnfsetfo  47502  mogoldbb  48255  uzlidlring  48705  2zlidl  48710