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 398

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 399

This theorem is referenced by:  marypha1lem  8889  acndom2  9472  ttukeylem6  9928  fpwwe2lem12  10055  swrdccatin1  14079  dfgcd2  15886  ramcl  16357  initoeu2lem1  17266  initoeu2  17268  gsmsymgreqlem2  18551  dfod2  18683  pgpfi  18722  ghmcyg  19008  psgndif  20738  scmatmulcl  21119  cpmatmcllem  21318  neiptoptop  21731  cncnp  21880  subislly  22081  ptcnplem  22221  pthaus  22238  xkohaus  22253  kqreglem1  22341  cnextcn  22667  qustgplem  22721  trust  22830  utoptop  22835  restutopopn  22839  utop3cls  22852  utopreg  22853  isucn2  22880  met1stc  23123  metustsym  23157  metuel2  23167  xrge0tsms  23434  xmetdcn2  23437  nmoleub2lem2  23712  iscfil2  23861  iscfil3  23868  dvmptfsum  24564  dvlip2  24584  aannenlem1  24909  ulm2  24965  ulmuni  24972  mtestbdd  24985  efopn  25233  dchrptlem1  25832  pntpbnd  26156  pntibnd  26161  f1otrg  26649  nbupgr  27118  upgriswlk  27414  usgr2pth  27537  clwwlkccatlem  27759  clwlkclwwlklem2a4  27767  cusconngr  27962  xrofsup  30484  ressprs  30635  gsummpt2d  30680  xrge0tsmsd  30685  omndmul2  30706  trsp2cyc  30758  isarchi3  30809  archirngz  30811  lmodslmd  30825  suborng  30881  isarchiofld  30883  dimkerim  31016  sqsscirc1  31144  lmxrge0  31188  lmdvg  31189  esumrnmpt2  31320  esumfsup  31322  esumcvg  31338  esum2d  31345  ddemeas  31488  omssubadd  31551  satffunlem1lem1  32642  satffunlem2lem1  32644  noetalem3  33212  btwnconn1lem13  33553  matunitlindflem1  34880  matunitlindflem2  34881  poimirlem29  34913  mblfinlem3  34923  mblfinlem4  34924  ftc1anclem7  34965  ftc1anc  34967  prdstotbnd  35064  ltrnid  37263  rencldnfilem  39407  pellex  39422  pellfundex  39473  dvdsacongtr  39571  fnchoice  41276  climsuse  41878  addlimc  41918  0ellimcdiv  41919  climxrre  42020  xlimmnfvlem2  42103  xlimpnfvlem2  42107  icccncfext  42159  dvnprodlem3  42222  fourierdlem12  42394  fourierdlem34  42416  fourierdlem50  42431  fourierdlem80  42461  fourierdlem81  42462  fourierdlem87  42468  etransclem35  42544  sge0pr  42666  meaiuninc3v  42756  smfmullem3  43058  mogoldbb  43940  uzlidlring  44190  2zlidl  44195