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  8615  marypha1lem  9340  acndom2  9968  ttukeylem6  10428  fpwwe2lem11  10556  swrdccatin1  14652  dfgcd2  16477  ramcl  16961  initoeu2lem1  17942  initoeu2  17944  chnind  18548  gsmsymgreqlem2  19364  dfod2  19497  pgpfi  19538  ghmcyg  19829  omndmul2  20066  suborng  20813  rhmpreimaidl  21236  psgndif  21561  mhpmulcl  22096  scmatmulcl  22466  cpmatmcllem  22666  neiptoptop  23079  cncnp  23228  subislly  23429  ptcnplem  23569  pthaus  23586  xkohaus  23601  kqreglem1  23689  cnextcn  24015  qustgplem  24069  trust  24177  utoptop  24182  restutopopn  24186  utop3cls  24199  utopreg  24200  isucn2  24226  met1stc  24469  metustsym  24503  metuel2  24513  xrge0tsms  24783  xmetdcn2  24786  nmoleub2lem2  25076  iscfil2  25226  iscfil3  25233  dvmptfsum  25939  dvlip2  25960  aannenlem1  26296  ulm2  26354  ulmuni  26361  mtestbdd  26374  efopn  26627  dchrptlem1  27235  pntpbnd  27559  pntibnd  27564  noetasuplem4  27708  f1otrg  28926  nbupgr  29400  upgriswlk  29697  usgr2pth  29820  clwwlkccatlem  30047  clwlkclwwlklem2a4  30055  cusconngr  30249  xrofsup  32828  ressprs  33029  gsummpt2d  33113  gsumfs2d  33125  xrge0tsmsd  33136  trsp2cyc  33186  isarchi3  33250  archirngz  33252  isarchiofld  33262  lmodslmd  33267  elrgspnlem4  33308  idlinsubrg  33493  rhmimaidl  33494  dimkerim  33765  sqsscirc1  34046  lmxrge0  34090  lmdvg  34091  esumrnmpt2  34206  esumfsup  34208  esumcvg  34224  esum2d  34231  ddemeas  34374  omssubadd  34438  satffunlem1lem1  35577  satffunlem2lem1  35579  btwnconn1lem13  36274  matunitlindflem1  37788  matunitlindflem2  37789  poimirlem29  37821  mblfinlem3  37831  mblfinlem4  37832  ftc1anclem7  37871  ftc1anc  37873  prdstotbnd  37966  ltrnid  40432  primrootscoprmpow  42390  posbezout  42391  primrootspoweq0  42397  aks6d1c6lem3  42463  unitscyglem3  42488  rencldnfilem  43098  pellex  43113  pellfundex  43164  dvdsacongtr  43262  naddcnff  43640  naddcnfid1  43645  oaun3lem1  43652  fnchoice  45310  climsuse  45890  addlimc  45928  0ellimcdiv  45929  climxrre  46030  xlimmnfvlem2  46113  xlimpnfvlem2  46117  icccncfext  46167  dvnprodlem3  46228  fourierdlem12  46399  fourierdlem34  46421  fourierdlem50  46436  fourierdlem80  46466  fourierdlem81  46467  fourierdlem87  46473  etransclem35  46549  sge0pr  46674  meaiuninc3v  46764  smfmullem3  47073  fsupdm  47122  finfdm  47126  cfsetsnfsetfo  47342  mogoldbb  48067  uzlidlring  48517  2zlidl  48522