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 731	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  8741  marypha1lem  9502  acndom2  10123  ttukeylem6  10583  fpwwe2lem11  10710  swrdccatin1  14773  dfgcd2  16593  ramcl  17076  initoeu2lem1  18081  initoeu2  18083  gsmsymgreqlem2  19473  dfod2  19606  pgpfi  19647  ghmcyg  19938  rhmpreimaidl  21310  psgndif  21643  mhpmulcl  22176  scmatmulcl  22545  cpmatmcllem  22745  neiptoptop  23160  cncnp  23309  subislly  23510  ptcnplem  23650  pthaus  23667  xkohaus  23682  kqreglem1  23770  cnextcn  24096  qustgplem  24150  trust  24259  utoptop  24264  restutopopn  24268  utop3cls  24281  utopreg  24282  isucn2  24309  met1stc  24555  metustsym  24589  metuel2  24599  xrge0tsms  24875  xmetdcn2  24878  nmoleub2lem2  25168  iscfil2  25319  iscfil3  25326  dvmptfsum  26033  dvlip2  26054  aannenlem1  26388  ulm2  26446  ulmuni  26453  mtestbdd  26466  efopn  26718  dchrptlem1  27326  pntpbnd  27650  pntibnd  27655  noetasuplem4  27799  f1otrg  28897  nbupgr  29379  upgriswlk  29677  usgr2pth  29800  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  cusconngr  30223  xrofsup  32774  ressprs  32936  chnind  32983  gsummpt2d  33032  xrge0tsmsd  33041  omndmul2  33062  trsp2cyc  33116  isarchi3  33167  archirngz  33169  lmodslmd  33183  suborng  33310  isarchiofld  33312  idlinsubrg  33424  rhmimaidl  33425  dimkerim  33640  sqsscirc1  33854  lmxrge0  33898  lmdvg  33899  esumrnmpt2  34032  esumfsup  34034  esumcvg  34050  esum2d  34057  ddemeas  34200  omssubadd  34265  satffunlem1lem1  35370  satffunlem2lem1  35372  btwnconn1lem13  36063  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem29  37609  mblfinlem3  37619  mblfinlem4  37620  ftc1anclem7  37659  ftc1anc  37661  prdstotbnd  37754  ltrnid  40092  primrootscoprmpow  42056  posbezout  42057  primrootspoweq0  42063  aks6d1c6lem3  42129  unitscyglem3  42154  rencldnfilem  42776  pellex  42791  pellfundex  42842  dvdsacongtr  42941  naddcnff  43324  naddcnfid1  43329  oaun3lem1  43336  fnchoice  44929  climsuse  45529  addlimc  45569  0ellimcdiv  45570  climxrre  45671  xlimmnfvlem2  45754  xlimpnfvlem2  45758  icccncfext  45808  dvnprodlem3  45869  fourierdlem12  46040  fourierdlem34  46062  fourierdlem50  46077  fourierdlem80  46107  fourierdlem81  46108  fourierdlem87  46114  etransclem35  46190  sge0pr  46315  meaiuninc3v  46405  smfmullem3  46714  fsupdm  46763  finfdm  46767  cfsetsnfsetfo  46975  mogoldbb  47659  uzlidlring  47958  2zlidl  47963