Theorem simp-4l 780

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  marypha1lem  9192  acndom2  9810  ttukeylem6  10270  fpwwe2lem11  10397  swrdccatin1  14438  dfgcd2  16254  ramcl  16730  initoeu2lem1  17729  initoeu2  17731  gsmsymgreqlem2  19039  dfod2  19171  pgpfi  19210  ghmcyg  19497  psgndif  20807  mhpmulcl  21339  scmatmulcl  21667  cpmatmcllem  21867  neiptoptop  22282  cncnp  22431  subislly  22632  ptcnplem  22772  pthaus  22789  xkohaus  22804  kqreglem1  22892  cnextcn  23218  qustgplem  23272  trust  23381  utoptop  23386  restutopopn  23390  utop3cls  23403  utopreg  23404  isucn2  23431  met1stc  23677  metustsym  23711  metuel2  23721  xrge0tsms  23997  xmetdcn2  24000  nmoleub2lem2  24279  iscfil2  24430  iscfil3  24437  dvmptfsum  25139  dvlip2  25159  aannenlem1  25488  ulm2  25544  ulmuni  25551  mtestbdd  25564  efopn  25813  dchrptlem1  26412  pntpbnd  26736  pntibnd  26741  f1otrg  27232  nbupgr  27711  upgriswlk  28008  usgr2pth  28132  clwwlkccatlem  28353  clwlkclwwlklem2a4  28361  cusconngr  28555  xrofsup  31090  ressprs  31241  gsummpt2d  31309  xrge0tsmsd  31317  omndmul2  31338  trsp2cyc  31390  isarchi3  31441  archirngz  31443  lmodslmd  31457  suborng  31514  isarchiofld  31516  rhmpreimaidl  31603  idlinsubrg  31608  rhmimaidl  31609  dimkerim  31708  sqsscirc1  31858  lmxrge0  31902  lmdvg  31903  esumrnmpt2  32036  esumfsup  32038  esumcvg  32054  esum2d  32061  ddemeas  32204  omssubadd  32267  satffunlem1lem1  33364  satffunlem2lem1  33366  naddssim  33837  noetasuplem4  33939  btwnconn1lem13  34401  matunitlindflem1  35773  matunitlindflem2  35774  poimirlem29  35806  mblfinlem3  35816  mblfinlem4  35817  ftc1anclem7  35856  ftc1anc  35858  prdstotbnd  35952  ltrnid  38149  rencldnfilem  40642  pellex  40657  pellfundex  40708  dvdsacongtr  40806  fnchoice  42572  climsuse  43149  addlimc  43189  0ellimcdiv  43190  climxrre  43291  xlimmnfvlem2  43374  xlimpnfvlem2  43378  icccncfext  43428  dvnprodlem3  43489  fourierdlem12  43660  fourierdlem34  43682  fourierdlem50  43697  fourierdlem80  43727  fourierdlem81  43728  fourierdlem87  43734  etransclem35  43810  sge0pr  43932  meaiuninc3v  44022  smfmullem3  44327  cfsetsnfsetfo  44554  mogoldbb  45237  uzlidlring  45487  2zlidl  45492