Theorem simp-4l 782

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 732	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  8649  marypha1lem  9384  acndom2  10007  ttukeylem6  10467  fpwwe2lem11  10594  swrdccatin1  14690  dfgcd2  16516  ramcl  17000  initoeu2lem1  17976  initoeu2  17978  gsmsymgreqlem2  19361  dfod2  19494  pgpfi  19535  ghmcyg  19826  rhmpreimaidl  21187  psgndif  21511  mhpmulcl  22036  scmatmulcl  22405  cpmatmcllem  22605  neiptoptop  23018  cncnp  23167  subislly  23368  ptcnplem  23508  pthaus  23525  xkohaus  23540  kqreglem1  23628  cnextcn  23954  qustgplem  24008  trust  24117  utoptop  24122  restutopopn  24126  utop3cls  24139  utopreg  24140  isucn2  24166  met1stc  24409  metustsym  24443  metuel2  24453  xrge0tsms  24723  xmetdcn2  24726  nmoleub2lem2  25016  iscfil2  25166  iscfil3  25173  dvmptfsum  25879  dvlip2  25900  aannenlem1  26236  ulm2  26294  ulmuni  26301  mtestbdd  26314  efopn  26567  dchrptlem1  27175  pntpbnd  27499  pntibnd  27504  noetasuplem4  27648  f1otrg  28798  nbupgr  29271  upgriswlk  29569  usgr2pth  29694  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  cusconngr  30120  xrofsup  32690  ressprs  32890  chnind  32937  gsummpt2d  32989  gsumfs2d  32995  xrge0tsmsd  33002  omndmul2  33026  trsp2cyc  33080  isarchi3  33141  archirngz  33143  lmodslmd  33157  elrgspnlem4  33196  suborng  33293  isarchiofld  33295  idlinsubrg  33402  rhmimaidl  33403  dimkerim  33623  sqsscirc1  33898  lmxrge0  33942  lmdvg  33943  esumrnmpt2  34058  esumfsup  34060  esumcvg  34076  esum2d  34083  ddemeas  34226  omssubadd  34291  satffunlem1lem1  35389  satffunlem2lem1  35391  btwnconn1lem13  36087  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem29  37643  mblfinlem3  37653  mblfinlem4  37654  ftc1anclem7  37693  ftc1anc  37695  prdstotbnd  37788  ltrnid  40129  primrootscoprmpow  42087  posbezout  42088  primrootspoweq0  42094  aks6d1c6lem3  42160  unitscyglem3  42185  rencldnfilem  42808  pellex  42823  pellfundex  42874  dvdsacongtr  42973  naddcnff  43351  naddcnfid1  43356  oaun3lem1  43363  fnchoice  45023  climsuse  45606  addlimc  45646  0ellimcdiv  45647  climxrre  45748  xlimmnfvlem2  45831  xlimpnfvlem2  45835  icccncfext  45885  dvnprodlem3  45946  fourierdlem12  46117  fourierdlem34  46139  fourierdlem50  46154  fourierdlem80  46184  fourierdlem81  46185  fourierdlem87  46191  etransclem35  46267  sge0pr  46392  meaiuninc3v  46482  smfmullem3  46791  fsupdm  46840  finfdm  46844  cfsetsnfsetfo  47061  mogoldbb  47786  uzlidlring  48223  2zlidl  48228