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  8651  marypha1lem  9390  acndom2  10013  ttukeylem6  10473  fpwwe2lem11  10600  swrdccatin1  14696  dfgcd2  16522  ramcl  17006  initoeu2lem1  17982  initoeu2  17984  gsmsymgreqlem2  19367  dfod2  19500  pgpfi  19541  ghmcyg  19832  rhmpreimaidl  21193  psgndif  21517  mhpmulcl  22042  scmatmulcl  22411  cpmatmcllem  22611  neiptoptop  23024  cncnp  23173  subislly  23374  ptcnplem  23514  pthaus  23531  xkohaus  23546  kqreglem1  23634  cnextcn  23960  qustgplem  24014  trust  24123  utoptop  24128  restutopopn  24132  utop3cls  24145  utopreg  24146  isucn2  24172  met1stc  24415  metustsym  24449  metuel2  24459  xrge0tsms  24729  xmetdcn2  24732  nmoleub2lem2  25022  iscfil2  25172  iscfil3  25179  dvmptfsum  25885  dvlip2  25906  aannenlem1  26242  ulm2  26300  ulmuni  26307  mtestbdd  26320  efopn  26573  dchrptlem1  27181  pntpbnd  27505  pntibnd  27510  noetasuplem4  27654  f1otrg  28804  nbupgr  29277  upgriswlk  29575  usgr2pth  29700  clwwlkccatlem  29924  clwlkclwwlklem2a4  29932  cusconngr  30126  xrofsup  32696  ressprs  32896  chnind  32943  gsummpt2d  32995  gsumfs2d  33001  xrge0tsmsd  33008  omndmul2  33032  trsp2cyc  33086  isarchi3  33147  archirngz  33149  lmodslmd  33163  elrgspnlem4  33202  suborng  33299  isarchiofld  33301  idlinsubrg  33408  rhmimaidl  33409  dimkerim  33629  sqsscirc1  33904  lmxrge0  33948  lmdvg  33949  esumrnmpt2  34064  esumfsup  34066  esumcvg  34082  esum2d  34089  ddemeas  34232  omssubadd  34297  satffunlem1lem1  35389  satffunlem2lem1  35391  btwnconn1lem13  36082  matunitlindflem1  37605  matunitlindflem2  37606  poimirlem29  37638  mblfinlem3  37648  mblfinlem4  37649  ftc1anclem7  37688  ftc1anc  37690  prdstotbnd  37783  ltrnid  40124  primrootscoprmpow  42082  posbezout  42083  primrootspoweq0  42089  aks6d1c6lem3  42155  unitscyglem3  42180  rencldnfilem  42801  pellex  42816  pellfundex  42867  dvdsacongtr  42966  naddcnff  43344  naddcnfid1  43349  oaun3lem1  43356  fnchoice  45016  climsuse  45599  addlimc  45639  0ellimcdiv  45640  climxrre  45741  xlimmnfvlem2  45824  xlimpnfvlem2  45828  icccncfext  45878  dvnprodlem3  45939  fourierdlem12  46110  fourierdlem34  46132  fourierdlem50  46147  fourierdlem80  46177  fourierdlem81  46178  fourierdlem87  46184  etransclem35  46260  sge0pr  46385  meaiuninc3v  46475  smfmullem3  46784  fsupdm  46833  finfdm  46837  cfsetsnfsetfo  47051  mogoldbb  47776  uzlidlring  48213  2zlidl  48218