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  18798  ssdifidlprm  21642  2sqmo  27764  legso  29062  opphl  29230  cgrabasimass  29378  angmgmaddcpbl  29390  angmgmaddcl  29391  angmgmaddlid  29392  angmgmaddrid  29393  prlngmolem2  29431  f1otrg  29448  2ndresdju  33285  cyc3conja  33760  rloccring  33874  mxidlprm  34037  mxidlirred  34039  constrconj  34419  constrfin  34420  constrelextdg2  34421  cos9thpiminplylem2  34457  qtophaus  34510  esumcst  34737  dffltz  43713  smfmullem3  47846