Theorem simp-4l 781

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  naddssim  8715  marypha1lem  9476  acndom2  10097  ttukeylem6  10557  fpwwe2lem11  10684  swrdccatin1  14733  dfgcd2  16547  ramcl  17031  initoeu2lem1  18036  initoeu2  18038  gsmsymgreqlem2  19429  dfod2  19562  pgpfi  19603  ghmcyg  19894  rhmpreimaidl  21266  psgndif  21598  mhpmulcl  22143  scmatmulcl  22511  cpmatmcllem  22711  neiptoptop  23126  cncnp  23275  subislly  23476  ptcnplem  23616  pthaus  23633  xkohaus  23648  kqreglem1  23736  cnextcn  24062  qustgplem  24116  trust  24225  utoptop  24230  restutopopn  24234  utop3cls  24247  utopreg  24248  isucn2  24275  met1stc  24521  metustsym  24555  metuel2  24565  xrge0tsms  24841  xmetdcn2  24844  nmoleub2lem2  25134  iscfil2  25285  iscfil3  25292  dvmptfsum  25998  dvlip2  26019  aannenlem1  26356  ulm2  26414  ulmuni  26421  mtestbdd  26434  efopn  26685  dchrptlem1  27293  pntpbnd  27617  pntibnd  27622  noetasuplem4  27766  f1otrg  28798  nbupgr  29280  upgriswlk  29578  usgr2pth  29701  clwwlkccatlem  29922  clwlkclwwlklem2a4  29930  cusconngr  30124  xrofsup  32671  ressprs  32833  chnind  32880  gsummpt2d  32917  xrge0tsmsd  32926  omndmul2  32947  trsp2cyc  33001  isarchi3  33052  archirngz  33054  lmodslmd  33068  suborng  33193  isarchiofld  33195  idlinsubrg  33306  rhmimaidl  33307  dimkerim  33522  sqsscirc1  33723  lmxrge0  33767  lmdvg  33768  esumrnmpt2  33901  esumfsup  33903  esumcvg  33919  esum2d  33926  ddemeas  34069  omssubadd  34134  satffunlem1lem1  35230  satffunlem2lem1  35232  btwnconn1lem13  35923  matunitlindflem1  37317  matunitlindflem2  37318  poimirlem29  37350  mblfinlem3  37360  mblfinlem4  37361  ftc1anclem7  37400  ftc1anc  37402  prdstotbnd  37495  ltrnid  39834  primrootscoprmpow  41797  posbezout  41798  primrootspoweq0  41804  aks6d1c6lem3  41870  rencldnfilem  42477  pellex  42492  pellfundex  42543  dvdsacongtr  42642  naddcnff  43028  naddcnfid1  43033  oaun3lem1  43040  fnchoice  44628  climsuse  45229  addlimc  45269  0ellimcdiv  45270  climxrre  45371  xlimmnfvlem2  45454  xlimpnfvlem2  45458  icccncfext  45508  dvnprodlem3  45569  fourierdlem12  45740  fourierdlem34  45762  fourierdlem50  45777  fourierdlem80  45807  fourierdlem81  45808  fourierdlem87  45814  etransclem35  45890  sge0pr  46015  meaiuninc3v  46105  smfmullem3  46414  fsupdm  46463  finfdm  46467  cfsetsnfsetfo  46675  mogoldbb  47357  uzlidlring  47612  2zlidl  47617