Theorem simp-5l 785

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-5l	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simp-5l

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad5antr 735	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:  mhmmnd  19040  neiptopnei  23097  neitx  23572  ustex3sym  24183  restutop  24202  ustuqtop4  24209  utopreg  24217  xrge0tsms  24800  noetainflem4  27704  f1otrg  28939  nn0xmulclb  32844  xrge0tsmsd  33134  elrgspnlem4  33306  imaslmod  33413  elrspunidl  33488  rhmpreimaprmidl  33511  qsidomlem1  33512  mxidlprm  33530  1arithidom  33597  dfufd2  33610  extdg1id  33810  pstmxmet  34041  esumfsup  34214  esum2dlem  34236  esum2d  34237  omssubadd  34444  eulerpartlemgvv  34520  signstfvneq0  34716  satffunlem2lem1  35586  matunitlindflem2  37938  aks6d1c2p2  42558  dffltz  43067  eldioph2  43194  limcrecl  46059  icccncfext  46315  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem60  46488  fourierdlem77  46611  fourierdlem80  46614  fourierdlem103  46637  fourierdlem104  46638  etransclem35  46697