Theorem simp-4l 779

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 728	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 206  df-an 396

This theorem is referenced by:  marypha1lem  9122  acndom2  9741  ttukeylem6  10201  fpwwe2lem11  10328  swrdccatin1  14366  dfgcd2  16182  ramcl  16658  initoeu2lem1  17645  initoeu2  17647  gsmsymgreqlem2  18954  dfod2  19086  pgpfi  19125  ghmcyg  19412  psgndif  20719  mhpmulcl  21249  scmatmulcl  21575  cpmatmcllem  21775  neiptoptop  22190  cncnp  22339  subislly  22540  ptcnplem  22680  pthaus  22697  xkohaus  22712  kqreglem1  22800  cnextcn  23126  qustgplem  23180  trust  23289  utoptop  23294  restutopopn  23298  utop3cls  23311  utopreg  23312  isucn2  23339  met1stc  23583  metustsym  23617  metuel2  23627  xrge0tsms  23903  xmetdcn2  23906  nmoleub2lem2  24185  iscfil2  24335  iscfil3  24342  dvmptfsum  25044  dvlip2  25064  aannenlem1  25393  ulm2  25449  ulmuni  25456  mtestbdd  25469  efopn  25718  dchrptlem1  26317  pntpbnd  26641  pntibnd  26646  f1otrg  27136  nbupgr  27614  upgriswlk  27910  usgr2pth  28033  clwwlkccatlem  28254  clwlkclwwlklem2a4  28262  cusconngr  28456  xrofsup  30992  ressprs  31143  gsummpt2d  31211  xrge0tsmsd  31219  omndmul2  31240  trsp2cyc  31292  isarchi3  31343  archirngz  31345  lmodslmd  31359  suborng  31416  isarchiofld  31418  rhmpreimaidl  31505  idlinsubrg  31510  rhmimaidl  31511  dimkerim  31610  sqsscirc1  31760  lmxrge0  31804  lmdvg  31805  esumrnmpt2  31936  esumfsup  31938  esumcvg  31954  esum2d  31961  ddemeas  32104  omssubadd  32167  satffunlem1lem1  33264  satffunlem2lem1  33266  naddssim  33764  noetasuplem4  33866  btwnconn1lem13  34328  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem29  35733  mblfinlem3  35743  mblfinlem4  35744  ftc1anclem7  35783  ftc1anc  35785  prdstotbnd  35879  ltrnid  38076  rencldnfilem  40558  pellex  40573  pellfundex  40624  dvdsacongtr  40722  fnchoice  42461  climsuse  43039  addlimc  43079  0ellimcdiv  43080  climxrre  43181  xlimmnfvlem2  43264  xlimpnfvlem2  43268  icccncfext  43318  dvnprodlem3  43379  fourierdlem12  43550  fourierdlem34  43572  fourierdlem50  43587  fourierdlem80  43617  fourierdlem81  43618  fourierdlem87  43624  etransclem35  43700  sge0pr  43822  meaiuninc3v  43912  smfmullem3  44214  cfsetsnfsetfo  44441  mogoldbb  45125  uzlidlring  45375  2zlidl  45380