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 733	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  8612  marypha1lem  9337  acndom2  9965  ttukeylem6  10425  fpwwe2lem11  10553  swrdccatin1  14649  dfgcd2  16474  ramcl  16958  initoeu2lem1  17939  initoeu2  17941  chnind  18545  gsmsymgreqlem2  19364  dfod2  19497  pgpfi  19538  ghmcyg  19829  omndmul2  20066  suborng  20811  rhmpreimaidl  21234  psgndif  21559  mhpmulcl  22093  scmatmulcl  22461  cpmatmcllem  22661  neiptoptop  23074  cncnp  23223  subislly  23424  ptcnplem  23564  pthaus  23581  xkohaus  23596  kqreglem1  23684  cnextcn  24010  qustgplem  24064  trust  24172  utoptop  24177  restutopopn  24181  utop3cls  24194  utopreg  24195  isucn2  24221  met1stc  24464  metustsym  24498  metuel2  24508  xrge0tsms  24778  xmetdcn2  24781  nmoleub2lem2  25061  iscfil2  25211  iscfil3  25218  dvmptfsum  25920  dvlip2  25941  aannenlem1  26276  ulm2  26334  ulmuni  26341  mtestbdd  26354  efopn  26607  dchrptlem1  27215  pntpbnd  27539  pntibnd  27544  noetasuplem4  27688  f1otrg  28927  nbupgr  29401  upgriswlk  29698  usgr2pth  29821  clwwlkccatlem  30048  clwlkclwwlklem2a4  30056  cusconngr  30250  xrofsup  32830  ressprs  33031  gsummpt2d  33115  gsumfs2d  33127  xrge0tsmsd  33139  trsp2cyc  33189  isarchi3  33253  archirngz  33255  isarchiofld  33265  lmodslmd  33270  elrgspnlem4  33311  idlinsubrg  33496  rhmimaidl  33497  dimkerim  33777  sqsscirc1  34058  lmxrge0  34102  lmdvg  34103  esumrnmpt2  34218  esumfsup  34220  esumcvg  34236  esum2d  34243  ddemeas  34386  omssubadd  34450  satffunlem1lem1  35590  satffunlem2lem1  35592  btwnconn1lem13  36287  matunitlindflem1  37928  matunitlindflem2  37929  poimirlem29  37961  mblfinlem3  37971  mblfinlem4  37972  ftc1anclem7  38011  ftc1anc  38013  prdstotbnd  38106  ltrnid  40572  primrootscoprmpow  42530  posbezout  42531  primrootspoweq0  42537  aks6d1c6lem3  42603  unitscyglem3  42628  rencldnfilem  43251  pellex  43266  pellfundex  43317  dvdsacongtr  43415  naddcnff  43793  naddcnfid1  43798  oaun3lem1  43805  fnchoice  45463  climsuse  46042  addlimc  46080  0ellimcdiv  46081  climxrre  46182  xlimmnfvlem2  46265  xlimpnfvlem2  46269  icccncfext  46319  dvnprodlem3  46380  fourierdlem12  46551  fourierdlem34  46573  fourierdlem50  46588  fourierdlem80  46618  fourierdlem81  46619  fourierdlem87  46625  etransclem35  46701  sge0pr  46826  meaiuninc3v  46916  smfmullem3  47225  fsupdm  47274  finfdm  47278  cfsetsnfsetfo  47494  mogoldbb  48219  uzlidlring  48669  2zlidl  48674