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 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  8600  marypha1lem  9317  acndom2  9945  ttukeylem6  10405  fpwwe2lem11  10532  swrdccatin1  14632  dfgcd2  16457  ramcl  16941  initoeu2lem1  17921  initoeu2  17923  chnind  18527  gsmsymgreqlem2  19343  dfod2  19476  pgpfi  19517  ghmcyg  19808  omndmul2  20045  suborng  20791  rhmpreimaidl  21214  psgndif  21539  mhpmulcl  22064  scmatmulcl  22433  cpmatmcllem  22633  neiptoptop  23046  cncnp  23195  subislly  23396  ptcnplem  23536  pthaus  23553  xkohaus  23568  kqreglem1  23656  cnextcn  23982  qustgplem  24036  trust  24144  utoptop  24149  restutopopn  24153  utop3cls  24166  utopreg  24167  isucn2  24193  met1stc  24436  metustsym  24470  metuel2  24480  xrge0tsms  24750  xmetdcn2  24753  nmoleub2lem2  25043  iscfil2  25193  iscfil3  25200  dvmptfsum  25906  dvlip2  25927  aannenlem1  26263  ulm2  26321  ulmuni  26328  mtestbdd  26341  efopn  26594  dchrptlem1  27202  pntpbnd  27526  pntibnd  27531  noetasuplem4  27675  f1otrg  28849  nbupgr  29322  upgriswlk  29619  usgr2pth  29742  clwwlkccatlem  29969  clwlkclwwlklem2a4  29977  cusconngr  30171  xrofsup  32750  ressprs  32947  gsummpt2d  33029  gsumfs2d  33035  xrge0tsmsd  33042  trsp2cyc  33092  isarchi3  33156  archirngz  33158  isarchiofld  33168  lmodslmd  33173  elrgspnlem4  33212  idlinsubrg  33396  rhmimaidl  33397  dimkerim  33640  sqsscirc1  33921  lmxrge0  33965  lmdvg  33966  esumrnmpt2  34081  esumfsup  34083  esumcvg  34099  esum2d  34106  ddemeas  34249  omssubadd  34313  satffunlem1lem1  35446  satffunlem2lem1  35448  btwnconn1lem13  36143  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem29  37688  mblfinlem3  37698  mblfinlem4  37699  ftc1anclem7  37738  ftc1anc  37740  prdstotbnd  37833  ltrnid  40233  primrootscoprmpow  42191  posbezout  42192  primrootspoweq0  42198  aks6d1c6lem3  42264  unitscyglem3  42289  rencldnfilem  42912  pellex  42927  pellfundex  42978  dvdsacongtr  43076  naddcnff  43454  naddcnfid1  43459  oaun3lem1  43466  fnchoice  45125  climsuse  45707  addlimc  45745  0ellimcdiv  45746  climxrre  45847  xlimmnfvlem2  45930  xlimpnfvlem2  45934  icccncfext  45984  dvnprodlem3  46045  fourierdlem12  46216  fourierdlem34  46238  fourierdlem50  46253  fourierdlem80  46283  fourierdlem81  46284  fourierdlem87  46290  etransclem35  46366  sge0pr  46491  meaiuninc3v  46581  smfmullem3  46890  fsupdm  46939  finfdm  46943  cfsetsnfsetfo  47159  mogoldbb  47884  uzlidlring  48334  2zlidl  48339