Theorem simp-4l 795

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad4antr 745	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  naddssim  8673  marypha1lem  9403  acndom2  10104  ttukeylem6  10563  fpwwe2lem11  10697  swrdccatin1  14841  dfgcd2  16683  ramcl  17168  initoeu2lem1  18150  initoeu2  18152  chnind  18756  gsmsymgreqlem2  19606  dfod2  19739  pgpfi  19780  ghmcyg  20071  omndmul2  20308  suborng  21094  rhmpreimaidl  21532  psgndif  21869  mhpmulcl  22431  scmatmulcl  22794  matunitlindflem1  22955  matunitlindflem2  22956  cpmatmcllem  22997  neiptoptop  23410  cncnp  23559  subislly  23761  ptcnplem  23901  pthaus  23918  xkohaus  23933  kqreglem1  24021  cnextcn  24347  qustgplem  24401  trust  24509  utoptop  24514  restutopopn  24518  utop3cls  24531  utopreg  24532  isucn2  24558  met1stc  24801  metustsym  24835  metuel2  24845  xrge0tsms  25115  xmetdcn2  25118  nmoleub2lem2  25398  iscfil2  25548  iscfil3  25555  dvmptfsum  26256  dvlip2  26276  aannenlem1  26618  ulm2  26675  ulmuni  26682  mtestbdd  26695  efopn  26949  dchrptlem1  27554  pntpbnd  27878  pntibnd  27883  noetasuplem4  28026  f1otrg  29381  nbupgr  29858  upgriswlk  30154  usgr2pth  30283  clwwlkccatlem  30513  clwlkclwwlklem2a4  30521  cusconngr  30725  xrofsup  33292  ressprs  33460  gsummpt2d  33543  gsumfs2d  33555  xrge0tsmsd  33567  trsp2cyc  33617  isarchi3  33681  archirngz  33683  isarchiofld  33693  lmodslmd  33698  elrgspnlem4  33739  idlinsubrg  33914  rhmimaidl  33915  dimkerim  34192  sqsscirc1  34473  lmxrge0  34517  lmdvg  34518  esumrnmpt2  34633  esumfsup  34635  esumcvg  34651  esum2d  34658  ddemeas  34802  omssubadd  34866  satffunlem1lem1  36088  satffunlem2lem1  36090  btwnconn1lem13  36786  poimirlem29  38487  mblfinlem3  38497  mblfinlem4  38498  ftc1anclem7  38537  ftc1anc  38539  prdstotbnd  38648  ltrnid  41112  primrootscoprmpow  43069  posbezout  43070  primrootspoweq0  43076  aks6d1c6lem3  43142  unitscyglem3  43167  rencldnfilem  43765  pellex  43780  pellfundex  43831  dvdsacongtr  43929  naddcnff  44307  naddcnfid1  44312  oaun3lem1  44319  fnchoice  45967  climsuse  46542  addlimc  46580  0ellimcdiv  46581  climxrre  46682  xlimmnfvlem2  46765  xlimpnfvlem2  46769  icccncfext  46819  dvnprodlem3  46880  fourierdlem12  47051  fourierdlem34  47073  fourierdlem50  47088  fourierdlem80  47118  fourierdlem81  47119  fourierdlem87  47125  etransclem35  47201  sge0pr  47326  meaiuninc3v  47416  smfmullem3  47725  fsupdm  47774  finfdm  47778  cfsetsnfsetfo  48052  mogoldbb  48805  uzlidlring  49254  2zlidl  49259