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  8616  marypha1lem  9341  acndom2  9969  ttukeylem6  10429  fpwwe2lem11  10557  swrdccatin1  14653  dfgcd2  16478  ramcl  16962  initoeu2lem1  17943  initoeu2  17945  chnind  18549  gsmsymgreqlem2  19365  dfod2  19498  pgpfi  19539  ghmcyg  19830  omndmul2  20067  suborng  20814  rhmpreimaidl  21237  psgndif  21562  mhpmulcl  22097  scmatmulcl  22467  cpmatmcllem  22667  neiptoptop  23080  cncnp  23229  subislly  23430  ptcnplem  23570  pthaus  23587  xkohaus  23602  kqreglem1  23690  cnextcn  24016  qustgplem  24070  trust  24178  utoptop  24183  restutopopn  24187  utop3cls  24200  utopreg  24201  isucn2  24227  met1stc  24470  metustsym  24504  metuel2  24514  xrge0tsms  24784  xmetdcn2  24787  nmoleub2lem2  25077  iscfil2  25227  iscfil3  25234  dvmptfsum  25940  dvlip2  25961  aannenlem1  26297  ulm2  26355  ulmuni  26362  mtestbdd  26375  efopn  26628  dchrptlem1  27236  pntpbnd  27560  pntibnd  27565  noetasuplem4  27709  f1otrg  28948  nbupgr  29422  upgriswlk  29719  usgr2pth  29842  clwwlkccatlem  30069  clwlkclwwlklem2a4  30077  cusconngr  30271  xrofsup  32850  ressprs  33051  gsummpt2d  33135  gsumfs2d  33147  xrge0tsmsd  33159  trsp2cyc  33209  isarchi3  33273  archirngz  33275  isarchiofld  33285  lmodslmd  33290  elrgspnlem4  33331  idlinsubrg  33516  rhmimaidl  33517  dimkerim  33797  sqsscirc1  34078  lmxrge0  34122  lmdvg  34123  esumrnmpt2  34238  esumfsup  34240  esumcvg  34256  esum2d  34263  ddemeas  34406  omssubadd  34470  satffunlem1lem1  35609  satffunlem2lem1  35611  btwnconn1lem13  36306  matunitlindflem1  37830  matunitlindflem2  37831  poimirlem29  37863  mblfinlem3  37873  mblfinlem4  37874  ftc1anclem7  37913  ftc1anc  37915  prdstotbnd  38008  ltrnid  40474  primrootscoprmpow  42432  posbezout  42433  primrootspoweq0  42439  aks6d1c6lem3  42505  unitscyglem3  42530  rencldnfilem  43140  pellex  43155  pellfundex  43206  dvdsacongtr  43304  naddcnff  43682  naddcnfid1  43687  oaun3lem1  43694  fnchoice  45352  climsuse  45931  addlimc  45969  0ellimcdiv  45970  climxrre  46071  xlimmnfvlem2  46154  xlimpnfvlem2  46158  icccncfext  46208  dvnprodlem3  46269  fourierdlem12  46440  fourierdlem34  46462  fourierdlem50  46477  fourierdlem80  46507  fourierdlem81  46508  fourierdlem87  46514  etransclem35  46590  sge0pr  46715  meaiuninc3v  46805  smfmullem3  47114  fsupdm  47163  finfdm  47167  cfsetsnfsetfo  47383  mogoldbb  48108  uzlidlring  48558  2zlidl  48563