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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  marypha1lem  9027  acndom2  9633  ttukeylem6  10093  fpwwe2lem11  10220  swrdccatin1  14255  dfgcd2  16069  ramcl  16545  initoeu2lem1  17474  initoeu2  17476  gsmsymgreqlem2  18777  dfod2  18909  pgpfi  18948  ghmcyg  19235  psgndif  20518  mhpmulcl  21043  scmatmulcl  21369  cpmatmcllem  21569  neiptoptop  21982  cncnp  22131  subislly  22332  ptcnplem  22472  pthaus  22489  xkohaus  22504  kqreglem1  22592  cnextcn  22918  qustgplem  22972  trust  23081  utoptop  23086  restutopopn  23090  utop3cls  23103  utopreg  23104  isucn2  23130  met1stc  23373  metustsym  23407  metuel2  23417  xrge0tsms  23685  xmetdcn2  23688  nmoleub2lem2  23967  iscfil2  24117  iscfil3  24124  dvmptfsum  24826  dvlip2  24846  aannenlem1  25175  ulm2  25231  ulmuni  25238  mtestbdd  25251  efopn  25500  dchrptlem1  26099  pntpbnd  26423  pntibnd  26428  f1otrg  26916  nbupgr  27386  upgriswlk  27682  usgr2pth  27805  clwwlkccatlem  28026  clwlkclwwlklem2a4  28034  cusconngr  28228  xrofsup  30764  ressprs  30914  gsummpt2d  30982  xrge0tsmsd  30990  omndmul2  31011  trsp2cyc  31063  isarchi3  31114  archirngz  31116  lmodslmd  31130  suborng  31187  isarchiofld  31189  rhmpreimaidl  31271  idlinsubrg  31276  rhmimaidl  31277  dimkerim  31376  sqsscirc1  31526  lmxrge0  31570  lmdvg  31571  esumrnmpt2  31702  esumfsup  31704  esumcvg  31720  esum2d  31727  ddemeas  31870  omssubadd  31933  satffunlem1lem1  33031  satffunlem2lem1  33033  naddssim  33523  noetasuplem4  33625  btwnconn1lem13  34087  matunitlindflem1  35459  matunitlindflem2  35460  poimirlem29  35492  mblfinlem3  35502  mblfinlem4  35503  ftc1anclem7  35542  ftc1anc  35544  prdstotbnd  35638  ltrnid  37835  rencldnfilem  40286  pellex  40301  pellfundex  40352  dvdsacongtr  40450  fnchoice  42186  climsuse  42767  addlimc  42807  0ellimcdiv  42808  climxrre  42909  xlimmnfvlem2  42992  xlimpnfvlem2  42996  icccncfext  43046  dvnprodlem3  43107  fourierdlem12  43278  fourierdlem34  43300  fourierdlem50  43315  fourierdlem80  43345  fourierdlem81  43346  fourierdlem87  43352  etransclem35  43428  sge0pr  43550  meaiuninc3v  43640  smfmullem3  43942  cfsetsnfsetfo  44169  mogoldbb  44853  uzlidlring  45103  2zlidl  45108