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  18718  ssdifidlprm  21555  2sqmo  27681  legso  28949  opphl  29117  cgrabasimass  29265  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  prlngmolem2  29318  f1otrg  29335  2ndresdju  33130  cyc3conja  33605  rloccring  33719  mxidlprm  33881  mxidlirred  33883  constrconj  34263  constrfin  34264  constrelextdg2  34265  cos9thpiminplylem2  34301  qtophaus  34354  esumcst  34581  dffltz  43488  smfmullem3  47629