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  8899  acndom2  9482  ttukeylem6  9938  fpwwe2lem12  10065  swrdccatin1  14089  dfgcd2  15896  ramcl  16367  initoeu2lem1  17276  initoeu2  17278  gsmsymgreqlem2  18561  dfod2  18693  pgpfi  18732  ghmcyg  19018  psgndif  20748  scmatmulcl  21129  cpmatmcllem  21328  neiptoptop  21741  cncnp  21890  subislly  22091  ptcnplem  22231  pthaus  22248  xkohaus  22263  kqreglem1  22351  cnextcn  22677  qustgplem  22731  trust  22840  utoptop  22845  restutopopn  22849  utop3cls  22862  utopreg  22863  isucn2  22890  met1stc  23133  metustsym  23167  metuel2  23177  xrge0tsms  23444  xmetdcn2  23447  nmoleub2lem2  23722  iscfil2  23871  iscfil3  23878  dvmptfsum  24574  dvlip2  24594  aannenlem1  24919  ulm2  24975  ulmuni  24982  mtestbdd  24995  efopn  25243  dchrptlem1  25842  pntpbnd  26166  pntibnd  26171  f1otrg  26659  nbupgr  27128  upgriswlk  27424  usgr2pth  27547  clwwlkccatlem  27769  clwlkclwwlklem2a4  27777  cusconngr  27972  xrofsup  30494  ressprs  30644  gsummpt2d  30689  xrge0tsmsd  30694  omndmul2  30715  trsp2cyc  30767  isarchi3  30818  archirngz  30820  lmodslmd  30834  suborng  30890  isarchiofld  30892  dimkerim  31025  sqsscirc1  31153  lmxrge0  31197  lmdvg  31198  esumrnmpt2  31329  esumfsup  31331  esumcvg  31347  esum2d  31354  ddemeas  31497  omssubadd  31560  satffunlem1lem1  32651  satffunlem2lem1  32653  noetalem3  33221  btwnconn1lem13  33562  matunitlindflem1  34890  matunitlindflem2  34891  poimirlem29  34923  mblfinlem3  34933  mblfinlem4  34934  ftc1anclem7  34975  ftc1anc  34977  prdstotbnd  35074  ltrnid  37273  rencldnfilem  39424  pellex  39439  pellfundex  39490  dvdsacongtr  39588  fnchoice  41293  climsuse  41896  addlimc  41936  0ellimcdiv  41937  climxrre  42038  xlimmnfvlem2  42121  xlimpnfvlem2  42125  icccncfext  42177  dvnprodlem3  42240  fourierdlem12  42411  fourierdlem34  42433  fourierdlem50  42448  fourierdlem80  42478  fourierdlem81  42479  fourierdlem87  42485  etransclem35  42561  sge0pr  42683  meaiuninc3v  42773  smfmullem3  43075  mogoldbb  43957  uzlidlring  44207  2zlidl  44212