Theorem simp-9r 806

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-9r	⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)

Proof of Theorem simp-9r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad9antlr 756	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:  legso  29044  miriso  29124  footexALT  29175  footex  29178  tgaaddcpbllem1  29331  cgraer  29359  cgrabasimass  29360  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  prlngmolem2  29413  f1otrg  29430  2ndresdju  33225  rloccring  33814  qsdrngi  34001  1arithidom  34051  constrfin  34360