Theorem simp-4l 782

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 731	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  naddssim  8684  marypha1lem  9428  acndom2  10049  ttukeylem6  10509  fpwwe2lem11  10636  swrdccatin1  14675  dfgcd2  16488  ramcl  16962  initoeu2lem1  17964  initoeu2  17966  gsmsymgreqlem2  19299  dfod2  19432  pgpfi  19473  ghmcyg  19764  psgndif  21155  mhpmulcl  21692  scmatmulcl  22020  cpmatmcllem  22220  neiptoptop  22635  cncnp  22784  subislly  22985  ptcnplem  23125  pthaus  23142  xkohaus  23157  kqreglem1  23245  cnextcn  23571  qustgplem  23625  trust  23734  utoptop  23739  restutopopn  23743  utop3cls  23756  utopreg  23757  isucn2  23784  met1stc  24030  metustsym  24064  metuel2  24074  xrge0tsms  24350  xmetdcn2  24353  nmoleub2lem2  24632  iscfil2  24783  iscfil3  24790  dvmptfsum  25492  dvlip2  25512  aannenlem1  25841  ulm2  25897  ulmuni  25904  mtestbdd  25917  efopn  26166  dchrptlem1  26767  pntpbnd  27091  pntibnd  27096  noetasuplem4  27239  f1otrg  28153  nbupgr  28632  upgriswlk  28929  usgr2pth  29052  clwwlkccatlem  29273  clwlkclwwlklem2a4  29281  cusconngr  29475  xrofsup  32011  ressprs  32164  gsummpt2d  32232  xrge0tsmsd  32240  omndmul2  32261  trsp2cyc  32313  isarchi3  32364  archirngz  32366  lmodslmd  32380  suborng  32464  isarchiofld  32466  rhmpreimaidl  32568  idlinsubrg  32580  rhmimaidl  32581  dimkerim  32743  sqsscirc1  32919  lmxrge0  32963  lmdvg  32964  esumrnmpt2  33097  esumfsup  33099  esumcvg  33115  esum2d  33122  ddemeas  33265  omssubadd  33330  satffunlem1lem1  34424  satffunlem2lem1  34426  btwnconn1lem13  35102  matunitlindflem1  36532  matunitlindflem2  36533  poimirlem29  36565  mblfinlem3  36575  mblfinlem4  36576  ftc1anclem7  36615  ftc1anc  36617  prdstotbnd  36710  ltrnid  39054  rencldnfilem  41606  pellex  41621  pellfundex  41672  dvdsacongtr  41771  naddcnff  42160  naddcnfid1  42165  oaun3lem1  42172  fnchoice  43761  climsuse  44372  addlimc  44412  0ellimcdiv  44413  climxrre  44514  xlimmnfvlem2  44597  xlimpnfvlem2  44601  icccncfext  44651  dvnprodlem3  44712  fourierdlem12  44883  fourierdlem34  44905  fourierdlem50  44920  fourierdlem80  44950  fourierdlem81  44951  fourierdlem87  44957  etransclem35  45033  sge0pr  45158  meaiuninc3v  45248  smfmullem3  45557  fsupdm  45606  finfdm  45610  cfsetsnfsetfo  45818  mogoldbb  46501  uzlidlring  46875  2zlidl  46880