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  8610  marypha1lem  9335  acndom2  9965  ttukeylem6  10425  fpwwe2lem11  10553  swrdccatin1  14676  dfgcd2  16504  ramcl  16989  initoeu2lem1  17970  initoeu2  17972  chnind  18576  gsmsymgreqlem2  19395  dfod2  19528  pgpfi  19569  ghmcyg  19860  omndmul2  20097  suborng  20842  rhmpreimaidl  21264  psgndif  21571  mhpmulcl  22104  scmatmulcl  22471  cpmatmcllem  22671  neiptoptop  23084  cncnp  23233  subislly  23434  ptcnplem  23574  pthaus  23591  xkohaus  23606  kqreglem1  23694  cnextcn  24020  qustgplem  24074  trust  24182  utoptop  24187  restutopopn  24191  utop3cls  24204  utopreg  24205  isucn2  24231  met1stc  24474  metustsym  24508  metuel2  24518  xrge0tsms  24788  xmetdcn2  24791  nmoleub2lem2  25071  iscfil2  25221  iscfil3  25228  dvmptfsum  25930  dvlip2  25950  aannenlem1  26282  ulm2  26338  ulmuni  26345  mtestbdd  26358  efopn  26610  dchrptlem1  27215  pntpbnd  27539  pntibnd  27544  noetasuplem4  27688  f1otrg  28927  nbupgr  29401  upgriswlk  29697  usgr2pth  29820  clwwlkccatlem  30047  clwlkclwwlklem2a4  30055  cusconngr  30249  xrofsup  32828  ressprs  33014  gsummpt2d  33098  gsumfs2d  33110  xrge0tsmsd  33122  trsp2cyc  33172  isarchi3  33236  archirngz  33238  isarchiofld  33248  lmodslmd  33253  elrgspnlem4  33294  idlinsubrg  33479  rhmimaidl  33480  dimkerim  33759  sqsscirc1  34040  lmxrge0  34084  lmdvg  34085  esumrnmpt2  34200  esumfsup  34202  esumcvg  34218  esum2d  34225  ddemeas  34368  omssubadd  34432  satffunlem1lem1  35572  satffunlem2lem1  35574  btwnconn1lem13  36269  matunitlindflem1  37925  matunitlindflem2  37926  poimirlem29  37958  mblfinlem3  37968  mblfinlem4  37969  ftc1anclem7  38008  ftc1anc  38010  prdstotbnd  38103  ltrnid  40569  primrootscoprmpow  42526  posbezout  42527  primrootspoweq0  42533  aks6d1c6lem3  42599  unitscyglem3  42624  rencldnfilem  43236  pellex  43251  pellfundex  43302  dvdsacongtr  43400  naddcnff  43778  naddcnfid1  43783  oaun3lem1  43790  fnchoice  45448  climsuse  46026  addlimc  46064  0ellimcdiv  46065  climxrre  46166  xlimmnfvlem2  46249  xlimpnfvlem2  46253  icccncfext  46303  dvnprodlem3  46364  fourierdlem12  46535  fourierdlem34  46557  fourierdlem50  46572  fourierdlem80  46602  fourierdlem81  46603  fourierdlem87  46609  etransclem35  46685  sge0pr  46810  meaiuninc3v  46900  smfmullem3  47209  fsupdm  47258  finfdm  47262  cfsetsnfsetfo  47496  mogoldbb  48249  uzlidlring  48699  2zlidl  48704