Theorem simp-8r 803

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 753	1 ⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  chnso  18681  ssdifidlprm  21467  2sqmo  27579  legso  28846  opphl  29013  prlngmolem2  29181  f1otrg  29198  2ndresdju  32972  cyc3conja  33455  rloccring  33569  mxidlprm  33731  mxidlirred  33733  constrconj  34113  constrfin  34114  constrelextdg2  34115  cos9thpiminplylem2  34151  qtophaus  34204  esumcst  34431  dffltz  43346  smfmullem3  47487