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  8695  marypha1lem  9425  acndom2  10133  ttukeylem6  10592  fpwwe2lem11  10726  swrdccatin1  14874  dfgcd2  16719  ramcl  17207  initoeu2lem1  18189  initoeu2  18191  chnind  18795  gsmsymgreqlem2  19645  dfod2  19778  pgpfi  19819  ghmcyg  20110  omndmul2  20347  suborng  21133  rhmpreimaidl  21571  psgndif  21908  mhpmulcl  22470  scmatmulcl  22833  matunitlindflem1  22994  matunitlindflem2  22995  cpmatmcllem  23036  neiptoptop  23449  cncnp  23598  subislly  23800  ptcnplem  23940  pthaus  23957  xkohaus  23972  kqreglem1  24060  cnextcn  24386  qustgplem  24440  trust  24548  utoptop  24553  restutopopn  24557  utop3cls  24570  utopreg  24571  isucn2  24597  met1stc  24840  metustsym  24874  metuel2  24884  xrge0tsms  25154  xmetdcn2  25157  nmoleub2lem2  25437  iscfil2  25587  iscfil3  25594  dvmptfsum  26295  dvlip2  26315  aannenlem1  26655  ulm2  26712  ulmuni  26719  mtestbdd  26732  efopn  26986  dchrptlem1  27591  pntpbnd  27915  pntibnd  27920  noetasuplem4  28093  f1otrg  29448  nbupgr  29925  upgriswlk  30221  usgr2pth  30350  clwwlkccatlem  30580  clwlkclwwlklem2a4  30588  cusconngr  30792  xrofsup  33401  ressprs  33569  gsummpt2d  33652  gsumfs2d  33664  xrge0tsmsd  33676  trsp2cyc  33726  isarchi3  33790  archirngz  33792  isarchiofld  33802  lmodslmd  33807  elrgspnlem4  33848  idlinsubrg  34023  rhmimaidl  34024  dimkerim  34301  sqsscirc1  34582  lmxrge0  34626  lmdvg  34627  esumrnmpt2  34742  esumfsup  34744  esumcvg  34760  esum2d  34767  ddemeas  34911  omssubadd  34974  satffunlem1lem1  36209  satffunlem2lem1  36211  btwnconn1lem13  36906  poimirlem29  38610  mblfinlem3  38620  mblfinlem4  38621  ftc1anclem7  38660  ftc1anc  38662  prdstotbnd  38771  ltrnid  41235  primrootscoprmpow  43192  posbezout  43193  primrootspoweq0  43199  aks6d1c6lem3  43265  unitscyglem3  43290  rencldnfilem  43870  pellex  43885  pellfundex  43936  dvdsacongtr  44034  naddcnff  44407  naddcnfid1  44412  oaun3lem1  44419  fnchoice  46089  climsuse  46663  addlimc  46701  0ellimcdiv  46702  climxrre  46803  xlimmnfvlem2  46886  xlimpnfvlem2  46890  icccncfext  46940  dvnprodlem3  47001  fourierdlem12  47172  fourierdlem34  47194  fourierdlem50  47209  fourierdlem80  47239  fourierdlem81  47240  fourierdlem87  47246  etransclem35  47322  sge0pr  47447  meaiuninc3v  47537  smfmullem3  47846  fsupdm  47895  finfdm  47899  cfsetsnfsetfo  48173  mogoldbb  48926  uzlidlring  49375  2zlidl  49380