Theorem simp-4l 781

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  naddssim  8683  marypha1lem  9427  acndom2  10048  ttukeylem6  10508  fpwwe2lem11  10635  swrdccatin1  14674  dfgcd2  16487  ramcl  16961  initoeu2lem1  17963  initoeu2  17965  gsmsymgreqlem2  19298  dfod2  19431  pgpfi  19472  ghmcyg  19763  psgndif  21154  mhpmulcl  21691  scmatmulcl  22019  cpmatmcllem  22219  neiptoptop  22634  cncnp  22783  subislly  22984  ptcnplem  23124  pthaus  23141  xkohaus  23156  kqreglem1  23244  cnextcn  23570  qustgplem  23624  trust  23733  utoptop  23738  restutopopn  23742  utop3cls  23755  utopreg  23756  isucn2  23783  met1stc  24029  metustsym  24063  metuel2  24073  xrge0tsms  24349  xmetdcn2  24352  nmoleub2lem2  24631  iscfil2  24782  iscfil3  24789  dvmptfsum  25491  dvlip2  25511  aannenlem1  25840  ulm2  25896  ulmuni  25903  mtestbdd  25916  efopn  26165  dchrptlem1  26764  pntpbnd  27088  pntibnd  27093  noetasuplem4  27236  f1otrg  28119  nbupgr  28598  upgriswlk  28895  usgr2pth  29018  clwwlkccatlem  29239  clwlkclwwlklem2a4  29247  cusconngr  29441  xrofsup  31975  ressprs  32128  gsummpt2d  32196  xrge0tsmsd  32204  omndmul2  32225  trsp2cyc  32277  isarchi3  32328  archirngz  32330  lmodslmd  32344  suborng  32428  isarchiofld  32430  rhmpreimaidl  32532  idlinsubrg  32544  rhmimaidl  32545  dimkerim  32707  sqsscirc1  32883  lmxrge0  32927  lmdvg  32928  esumrnmpt2  33061  esumfsup  33063  esumcvg  33079  esum2d  33086  ddemeas  33229  omssubadd  33294  satffunlem1lem1  34388  satffunlem2lem1  34390  btwnconn1lem13  35066  matunitlindflem1  36479  matunitlindflem2  36480  poimirlem29  36512  mblfinlem3  36522  mblfinlem4  36523  ftc1anclem7  36562  ftc1anc  36564  prdstotbnd  36657  ltrnid  39001  rencldnfilem  41548  pellex  41563  pellfundex  41614  dvdsacongtr  41713  naddcnff  42102  naddcnfid1  42107  oaun3lem1  42114  fnchoice  43703  climsuse  44314  addlimc  44354  0ellimcdiv  44355  climxrre  44456  xlimmnfvlem2  44539  xlimpnfvlem2  44543  icccncfext  44593  dvnprodlem3  44654  fourierdlem12  44825  fourierdlem34  44847  fourierdlem50  44862  fourierdlem80  44892  fourierdlem81  44893  fourierdlem87  44899  etransclem35  44975  sge0pr  45100  meaiuninc3v  45190  smfmullem3  45499  fsupdm  45548  finfdm  45552  cfsetsnfsetfo  45760  mogoldbb  46443  uzlidlring  46817  2zlidl  46822