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  18827  ssdifidlprm  21672  2sqmo  27794  legso  29092  opphl  29260  cgrabasimass  29408  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddlid  29422  angmgmaddrid  29423  prlngmolem2  29461  f1otrg  29478  2ndresdju  33315  cyc3conja  33788  rloccring  33902  mxidlprm  34065  mxidlirred  34067  constrconj  34447  constrfin  34448  constrelextdg2  34449  cos9thpiminplylem2  34485  qtophaus  34538  esumcst  34765  dffltz  43863  smfmullem3  48008