Theorem simp-4l 802

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4l	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		simplll 794	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	adantr 480	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simp-5l  804  marypha1lem  8222  acndom2  8760  ttukeylem6  9219  fpwwe2lem12  9342  reuccats1  13332  dfgcd2  15101  ramcl  15571  initoeu2lem1  16487  gsmsymgreqlem2  17674  dfod2  17804  pgpfi  17843  ghmcyg  18120  psgndif  19767  scmatmulcl  20143  cpmatmcllem  20342  neiptoptop  20745  cncnp  20894  subislly  21094  ptcnplem  21234  pthaus  21251  xkohaus  21266  kqreglem1  21354  cnextcn  21681  qustgplem  21734  trust  21843  utoptop  21848  restutopopn  21852  ustuqtop2  21856  ustuqtop3  21857  utop3cls  21865  utopreg  21866  isucn2  21893  met1stc  22136  metustsym  22170  metuel2  22180  xrge0tsms  22445  xmetdcn2  22448  nmoleub2lem2  22724  iscfil2  22872  iscfil3  22879  dvmptfsum  23542  dvlip2  23562  aannenlem1  23887  ulm2  23943  ulmuni  23950  mtestbdd  23963  efopn  24204  dchrptlem1  24789  pntpbnd  25077  pntibnd  25082  f1otrg  25551  f1otrge  25552  pthdepisspth  26104  usgra2adedgwlkonALT  26144  cusconngra  26204  clwlkisclwwlklem2a4  26312  xrofsup  28923  ressprs  28986  omndmul2  29043  isarchi3  29072  archirngz  29074  lmodslmd  29088  gsummpt2d  29112  xrge0tsmsd  29116  suborng  29146  isarchiofld  29148  sqsscirc1  29282  lmxrge0  29326  lmdvg  29327  esumrnmpt2  29457  esumfsup  29459  esumcvg  29475  esum2d  29482  ddemeas  29626  omssubadd  29689  btwnconn1lem13  31376  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem29  32608  mblfinlem3  32618  mblfinlem4  32619  ftc1anclem7  32661  ftc1anc  32663  prdstotbnd  32763  ltrnid  34439  rencldnfilem  36402  pellex  36417  pellfundex  36468  dvdsacongtr  36569  fnchoice  38211  climsuse  38675  addlimc  38715  0ellimcdiv  38716  limclner  38718  icccncfext  38773  dvnprodlem3  38838  fourierdlem12  39012  fourierdlem34  39034  fourierdlem50  39049  fourierdlem80  39079  fourierdlem81  39080  fourierdlem87  39086  etransclem35  39162  sge0pr  39287  smfmullem3  39678  nbupgr  40566  usgr2pth  40970  clwlkclwwlklem2a4  41206  cusconngr  41358  uzlidlring  41719  2zlidl  41724