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 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 206  df-an 396

This theorem is referenced by:  naddssim  8699  marypha1lem  9448  acndom2  10069  ttukeylem6  10529  fpwwe2lem11  10656  swrdccatin1  14699  dfgcd2  16513  ramcl  16989  initoeu2lem1  17994  initoeu2  17996  gsmsymgreqlem2  19377  dfod2  19510  pgpfi  19551  ghmcyg  19842  psgndif  21521  mhpmulcl  22060  scmatmulcl  22407  cpmatmcllem  22607  neiptoptop  23022  cncnp  23171  subislly  23372  ptcnplem  23512  pthaus  23529  xkohaus  23544  kqreglem1  23632  cnextcn  23958  qustgplem  24012  trust  24121  utoptop  24126  restutopopn  24130  utop3cls  24143  utopreg  24144  isucn2  24171  met1stc  24417  metustsym  24451  metuel2  24461  xrge0tsms  24737  xmetdcn2  24740  nmoleub2lem2  25030  iscfil2  25181  iscfil3  25188  dvmptfsum  25894  dvlip2  25915  aannenlem1  26250  ulm2  26308  ulmuni  26315  mtestbdd  26328  efopn  26579  dchrptlem1  27184  pntpbnd  27508  pntibnd  27513  noetasuplem4  27656  f1otrg  28662  nbupgr  29144  upgriswlk  29442  usgr2pth  29565  clwwlkccatlem  29786  clwlkclwwlklem2a4  29794  cusconngr  29988  xrofsup  32521  ressprs  32672  gsummpt2d  32741  xrge0tsmsd  32749  omndmul2  32770  trsp2cyc  32822  isarchi3  32873  archirngz  32875  lmodslmd  32889  suborng  32970  isarchiofld  32972  rhmpreimaidl  33070  idlinsubrg  33082  rhmimaidl  33083  dimkerim  33257  sqsscirc1  33445  lmxrge0  33489  lmdvg  33490  esumrnmpt2  33623  esumfsup  33625  esumcvg  33641  esum2d  33648  ddemeas  33791  omssubadd  33856  satffunlem1lem1  34948  satffunlem2lem1  34950  btwnconn1lem13  35631  matunitlindflem1  37024  matunitlindflem2  37025  poimirlem29  37057  mblfinlem3  37067  mblfinlem4  37068  ftc1anclem7  37107  ftc1anc  37109  prdstotbnd  37202  ltrnid  39545  primrootscoprmpow  41506  posbezout  41507  aks6d1c6lem3  41576  rencldnfilem  42162  pellex  42177  pellfundex  42228  dvdsacongtr  42327  naddcnff  42714  naddcnfid1  42719  oaun3lem1  42726  fnchoice  44314  climsuse  44919  addlimc  44959  0ellimcdiv  44960  climxrre  45061  xlimmnfvlem2  45144  xlimpnfvlem2  45148  icccncfext  45198  dvnprodlem3  45259  fourierdlem12  45430  fourierdlem34  45452  fourierdlem50  45467  fourierdlem80  45497  fourierdlem81  45498  fourierdlem87  45504  etransclem35  45580  sge0pr  45705  meaiuninc3v  45795  smfmullem3  46104  fsupdm  46153  finfdm  46157  cfsetsnfsetfo  46365  mogoldbb  47048  uzlidlring  47220  2zlidl  47225