Theorem simp-4l 792

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 742	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  naddssim  8656  marypha1lem  9377  acndom2  10022  ttukeylem6  10482  fpwwe2lem11  10610  swrdccatin1  14748  dfgcd2  16590  ramcl  17075  initoeu2lem1  18057  initoeu2  18059  chnind  18663  gsmsymgreqlem2  19481  dfod2  19614  pgpfi  19655  ghmcyg  19946  omndmul2  20183  suborng  20932  rhmpreimaidl  21354  psgndif  21661  mhpmulcl  22221  scmatmulcl  22585  cpmatmcllem  22785  neiptoptop  23198  cncnp  23347  subislly  23548  ptcnplem  23688  pthaus  23705  xkohaus  23720  kqreglem1  23808  cnextcn  24134  qustgplem  24188  trust  24296  utoptop  24301  restutopopn  24305  utop3cls  24318  utopreg  24319  isucn2  24345  met1stc  24588  metustsym  24622  metuel2  24632  xrge0tsms  24902  xmetdcn2  24905  nmoleub2lem2  25185  iscfil2  25335  iscfil3  25342  dvmptfsum  26044  dvlip2  26064  aannenlem1  26399  ulm2  26455  ulmuni  26462  mtestbdd  26475  efopn  26730  dchrptlem1  27335  pntpbnd  27659  pntibnd  27664  noetasuplem4  27807  f1otrg  29078  nbupgr  29552  upgriswlk  29848  usgr2pth  29971  clwwlkccatlem  30198  clwlkclwwlklem2a4  30206  cusconngr  30400  xrofsup  32975  ressprs  33150  gsummpt2d  33235  gsumfs2d  33247  xrge0tsmsd  33259  trsp2cyc  33309  isarchi3  33373  archirngz  33375  isarchiofld  33385  lmodslmd  33390  elrgspnlem4  33432  idlinsubrg  33620  rhmimaidl  33621  dimkerim  33926  sqsscirc1  34207  lmxrge0  34251  lmdvg  34252  esumrnmpt2  34367  esumfsup  34369  esumcvg  34385  esum2d  34392  ddemeas  34535  omssubadd  34599  satffunlem1lem1  35757  satffunlem2lem1  35759  btwnconn1lem13  36454  matunitlindflem1  38120  matunitlindflem2  38121  poimirlem29  38153  mblfinlem3  38163  mblfinlem4  38164  ftc1anclem7  38203  ftc1anc  38205  prdstotbnd  38298  ltrnid  40764  primrootscoprmpow  42721  posbezout  42722  primrootspoweq0  42728  aks6d1c6lem3  42794  unitscyglem3  42819  rencldnfilem  43402  pellex  43417  pellfundex  43468  dvdsacongtr  43566  naddcnff  43944  naddcnfid1  43949  oaun3lem1  43956  fnchoice  45600  climsuse  46175  addlimc  46213  0ellimcdiv  46214  climxrre  46315  xlimmnfvlem2  46398  xlimpnfvlem2  46402  icccncfext  46452  dvnprodlem3  46513  fourierdlem12  46684  fourierdlem34  46706  fourierdlem50  46721  fourierdlem80  46751  fourierdlem81  46752  fourierdlem87  46758  etransclem35  46834  sge0pr  46959  meaiuninc3v  47049  smfmullem3  47358  fsupdm  47407  finfdm  47411  cfsetsnfsetfo  47645  mogoldbb  48398  uzlidlring  48848  2zlidl  48853