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  8606  marypha1lem  9323  acndom2  9951  ttukeylem6  10411  fpwwe2lem11  10538  swrdccatin1  14638  dfgcd2  16463  ramcl  16947  initoeu2lem1  17927  initoeu2  17929  chnind  18533  gsmsymgreqlem2  19349  dfod2  19482  pgpfi  19523  ghmcyg  19814  omndmul2  20051  suborng  20797  rhmpreimaidl  21220  psgndif  21545  mhpmulcl  22070  scmatmulcl  22439  cpmatmcllem  22639  neiptoptop  23052  cncnp  23201  subislly  23402  ptcnplem  23542  pthaus  23559  xkohaus  23574  kqreglem1  23662  cnextcn  23988  qustgplem  24042  trust  24150  utoptop  24155  restutopopn  24159  utop3cls  24172  utopreg  24173  isucn2  24199  met1stc  24442  metustsym  24476  metuel2  24486  xrge0tsms  24756  xmetdcn2  24759  nmoleub2lem2  25049  iscfil2  25199  iscfil3  25206  dvmptfsum  25912  dvlip2  25933  aannenlem1  26269  ulm2  26327  ulmuni  26334  mtestbdd  26347  efopn  26600  dchrptlem1  27208  pntpbnd  27532  pntibnd  27537  noetasuplem4  27681  f1otrg  28855  nbupgr  29329  upgriswlk  29626  usgr2pth  29749  clwwlkccatlem  29976  clwlkclwwlklem2a4  29984  cusconngr  30178  xrofsup  32757  ressprs  32954  gsummpt2d  33036  gsumfs2d  33042  xrge0tsmsd  33049  trsp2cyc  33099  isarchi3  33163  archirngz  33165  isarchiofld  33175  lmodslmd  33180  elrgspnlem4  33219  idlinsubrg  33403  rhmimaidl  33404  dimkerim  33647  sqsscirc1  33928  lmxrge0  33972  lmdvg  33973  esumrnmpt2  34088  esumfsup  34090  esumcvg  34106  esum2d  34113  ddemeas  34256  omssubadd  34320  satffunlem1lem1  35453  satffunlem2lem1  35455  btwnconn1lem13  36150  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem29  37695  mblfinlem3  37705  mblfinlem4  37706  ftc1anclem7  37745  ftc1anc  37747  prdstotbnd  37840  ltrnid  40240  primrootscoprmpow  42198  posbezout  42199  primrootspoweq0  42205  aks6d1c6lem3  42271  unitscyglem3  42296  rencldnfilem  42918  pellex  42933  pellfundex  42984  dvdsacongtr  43082  naddcnff  43460  naddcnfid1  43465  oaun3lem1  43472  fnchoice  45131  climsuse  45713  addlimc  45751  0ellimcdiv  45752  climxrre  45853  xlimmnfvlem2  45936  xlimpnfvlem2  45940  icccncfext  45990  dvnprodlem3  46051  fourierdlem12  46222  fourierdlem34  46244  fourierdlem50  46259  fourierdlem80  46289  fourierdlem81  46290  fourierdlem87  46296  etransclem35  46372  sge0pr  46497  meaiuninc3v  46587  smfmullem3  46896  fsupdm  46945  finfdm  46949  cfsetsnfsetfo  47165  mogoldbb  47890  uzlidlring  48340  2zlidl  48345