Theorem simp-8r 804

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

Assertion

Ref	Expression
simp-8r	⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Proof of Theorem simp-8r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad8antlr 754	1 ⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  chnso  18803  ssdifidlprm  21647  2sqmo  27769  legso  29067  opphl  29235  cgrabasimass  29383  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  angmgmaddrid  29398  prlngmolem2  29436  f1otrg  29453  2ndresdju  33290  cyc3conja  33764  rloccring  33878  mxidlprm  34041  mxidlirred  34043  constrconj  34423  constrfin  34424  constrelextdg2  34425  cos9thpiminplylem2  34461  qtophaus  34514  esumcst  34741  dffltz  43763  smfmullem3  47896