Theorem simp-4l 783

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 732	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 207  df-an 396

This theorem is referenced by:  naddssim  8723  marypha1lem  9473  acndom2  10094  ttukeylem6  10554  fpwwe2lem11  10681  swrdccatin1  14763  dfgcd2  16583  ramcl  17067  initoeu2lem1  18059  initoeu2  18061  gsmsymgreqlem2  19449  dfod2  19582  pgpfi  19623  ghmcyg  19914  rhmpreimaidl  21287  psgndif  21620  mhpmulcl  22153  scmatmulcl  22524  cpmatmcllem  22724  neiptoptop  23139  cncnp  23288  subislly  23489  ptcnplem  23629  pthaus  23646  xkohaus  23661  kqreglem1  23749  cnextcn  24075  qustgplem  24129  trust  24238  utoptop  24243  restutopopn  24247  utop3cls  24260  utopreg  24261  isucn2  24288  met1stc  24534  metustsym  24568  metuel2  24578  xrge0tsms  24856  xmetdcn2  24859  nmoleub2lem2  25149  iscfil2  25300  iscfil3  25307  dvmptfsum  26013  dvlip2  26034  aannenlem1  26370  ulm2  26428  ulmuni  26435  mtestbdd  26448  efopn  26700  dchrptlem1  27308  pntpbnd  27632  pntibnd  27637  noetasuplem4  27781  f1otrg  28879  nbupgr  29361  upgriswlk  29659  usgr2pth  29784  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  cusconngr  30210  xrofsup  32771  ressprs  32954  chnind  33001  gsummpt2d  33052  gsumfs2d  33058  xrge0tsmsd  33065  omndmul2  33089  trsp2cyc  33143  isarchi3  33194  archirngz  33196  lmodslmd  33210  elrgspnlem4  33249  suborng  33345  isarchiofld  33347  idlinsubrg  33459  rhmimaidl  33460  dimkerim  33678  sqsscirc1  33907  lmxrge0  33951  lmdvg  33952  esumrnmpt2  34069  esumfsup  34071  esumcvg  34087  esum2d  34094  ddemeas  34237  omssubadd  34302  satffunlem1lem1  35407  satffunlem2lem1  35409  btwnconn1lem13  36100  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem29  37656  mblfinlem3  37666  mblfinlem4  37667  ftc1anclem7  37706  ftc1anc  37708  prdstotbnd  37801  ltrnid  40137  primrootscoprmpow  42100  posbezout  42101  primrootspoweq0  42107  aks6d1c6lem3  42173  unitscyglem3  42198  rencldnfilem  42831  pellex  42846  pellfundex  42897  dvdsacongtr  42996  naddcnff  43375  naddcnfid1  43380  oaun3lem1  43387  fnchoice  45034  climsuse  45623  addlimc  45663  0ellimcdiv  45664  climxrre  45765  xlimmnfvlem2  45848  xlimpnfvlem2  45852  icccncfext  45902  dvnprodlem3  45963  fourierdlem12  46134  fourierdlem34  46156  fourierdlem50  46171  fourierdlem80  46201  fourierdlem81  46202  fourierdlem87  46208  etransclem35  46284  sge0pr  46409  meaiuninc3v  46499  smfmullem3  46808  fsupdm  46857  finfdm  46861  cfsetsnfsetfo  47072  mogoldbb  47772  uzlidlring  48151  2zlidl  48156