Theorem simp-4l 780

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  marypha1lem  9190  acndom2  9808  ttukeylem6  10268  fpwwe2lem11  10395  swrdccatin1  14436  dfgcd2  16252  ramcl  16728  initoeu2lem1  17727  initoeu2  17729  gsmsymgreqlem2  19037  dfod2  19169  pgpfi  19208  ghmcyg  19495  psgndif  20805  mhpmulcl  21337  scmatmulcl  21665  cpmatmcllem  21865  neiptoptop  22280  cncnp  22429  subislly  22630  ptcnplem  22770  pthaus  22787  xkohaus  22802  kqreglem1  22890  cnextcn  23216  qustgplem  23270  trust  23379  utoptop  23384  restutopopn  23388  utop3cls  23401  utopreg  23402  isucn2  23429  met1stc  23675  metustsym  23709  metuel2  23719  xrge0tsms  23995  xmetdcn2  23998  nmoleub2lem2  24277  iscfil2  24428  iscfil3  24435  dvmptfsum  25137  dvlip2  25157  aannenlem1  25486  ulm2  25542  ulmuni  25549  mtestbdd  25562  efopn  25811  dchrptlem1  26410  pntpbnd  26734  pntibnd  26739  f1otrg  27230  nbupgr  27709  upgriswlk  28006  usgr2pth  28129  clwwlkccatlem  28350  clwlkclwwlklem2a4  28358  cusconngr  28552  xrofsup  31087  ressprs  31238  gsummpt2d  31306  xrge0tsmsd  31314  omndmul2  31335  trsp2cyc  31387  isarchi3  31438  archirngz  31440  lmodslmd  31454  suborng  31511  isarchiofld  31513  rhmpreimaidl  31600  idlinsubrg  31605  rhmimaidl  31606  dimkerim  31705  sqsscirc1  31855  lmxrge0  31899  lmdvg  31900  esumrnmpt2  32033  esumfsup  32035  esumcvg  32051  esum2d  32058  ddemeas  32201  omssubadd  32264  satffunlem1lem1  33361  satffunlem2lem1  33363  naddssim  33834  noetasuplem4  33936  btwnconn1lem13  34398  matunitlindflem1  35770  matunitlindflem2  35771  poimirlem29  35803  mblfinlem3  35813  mblfinlem4  35814  ftc1anclem7  35853  ftc1anc  35855  prdstotbnd  35949  ltrnid  38146  rencldnfilem  40639  pellex  40654  pellfundex  40705  dvdsacongtr  40803  fnchoice  42542  climsuse  43119  addlimc  43159  0ellimcdiv  43160  climxrre  43261  xlimmnfvlem2  43344  xlimpnfvlem2  43348  icccncfext  43398  dvnprodlem3  43459  fourierdlem12  43630  fourierdlem34  43652  fourierdlem50  43667  fourierdlem80  43697  fourierdlem81  43698  fourierdlem87  43704  etransclem35  43780  sge0pr  43902  meaiuninc3v  43992  smfmullem3  44294  cfsetsnfsetfo  44521  mogoldbb  45204  uzlidlring  45454  2zlidl  45459