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  18778  ssdifidlprm  21622  2sqmo  27746  legso  29044  opphl  29212  cgrabasimass  29360  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  prlngmolem2  29413  f1otrg  29430  2ndresdju  33225  cyc3conja  33700  rloccring  33814  mxidlprm  33977  mxidlirred  33979  constrconj  34359  constrfin  34360  constrelextdg2  34361  cos9thpiminplylem2  34397  qtophaus  34450  esumcst  34677  dffltz  43624  smfmullem3  47747