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  8595  marypha1lem  9312  acndom2  9937  ttukeylem6  10397  fpwwe2lem11  10524  swrdccatin1  14624  dfgcd2  16449  ramcl  16933  initoeu2lem1  17913  initoeu2  17915  chnind  18519  gsmsymgreqlem2  19336  dfod2  19469  pgpfi  19510  ghmcyg  19801  omndmul2  20038  suborng  20784  rhmpreimaidl  21207  psgndif  21532  mhpmulcl  22057  scmatmulcl  22426  cpmatmcllem  22626  neiptoptop  23039  cncnp  23188  subislly  23389  ptcnplem  23529  pthaus  23546  xkohaus  23561  kqreglem1  23649  cnextcn  23975  qustgplem  24029  trust  24137  utoptop  24142  restutopopn  24146  utop3cls  24159  utopreg  24160  isucn2  24186  met1stc  24429  metustsym  24463  metuel2  24473  xrge0tsms  24743  xmetdcn2  24746  nmoleub2lem2  25036  iscfil2  25186  iscfil3  25193  dvmptfsum  25899  dvlip2  25920  aannenlem1  26256  ulm2  26314  ulmuni  26321  mtestbdd  26334  efopn  26587  dchrptlem1  27195  pntpbnd  27519  pntibnd  27524  noetasuplem4  27668  f1otrg  28842  nbupgr  29315  upgriswlk  29612  usgr2pth  29735  clwwlkccatlem  29959  clwlkclwwlklem2a4  29967  cusconngr  30161  xrofsup  32740  ressprs  32937  gsummpt2d  33019  gsumfs2d  33025  xrge0tsmsd  33032  trsp2cyc  33082  isarchi3  33146  archirngz  33148  isarchiofld  33158  lmodslmd  33163  elrgspnlem4  33202  idlinsubrg  33386  rhmimaidl  33387  dimkerim  33630  sqsscirc1  33911  lmxrge0  33955  lmdvg  33956  esumrnmpt2  34071  esumfsup  34073  esumcvg  34089  esum2d  34096  ddemeas  34239  omssubadd  34303  satffunlem1lem1  35414  satffunlem2lem1  35416  btwnconn1lem13  36112  matunitlindflem1  37635  matunitlindflem2  37636  poimirlem29  37668  mblfinlem3  37678  mblfinlem4  37679  ftc1anclem7  37718  ftc1anc  37720  prdstotbnd  37813  ltrnid  40153  primrootscoprmpow  42111  posbezout  42112  primrootspoweq0  42118  aks6d1c6lem3  42184  unitscyglem3  42209  rencldnfilem  42832  pellex  42847  pellfundex  42898  dvdsacongtr  42996  naddcnff  43374  naddcnfid1  43379  oaun3lem1  43386  fnchoice  45045  climsuse  45627  addlimc  45665  0ellimcdiv  45666  climxrre  45767  xlimmnfvlem2  45850  xlimpnfvlem2  45854  icccncfext  45904  dvnprodlem3  45965  fourierdlem12  46136  fourierdlem34  46158  fourierdlem50  46173  fourierdlem80  46203  fourierdlem81  46204  fourierdlem87  46210  etransclem35  46286  sge0pr  46411  meaiuninc3v  46501  smfmullem3  46810  fsupdm  46859  finfdm  46863  cfsetsnfsetfo  47070  mogoldbb  47795  uzlidlring  48245  2zlidl  48250