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  29067  miriso  29147  footexALT  29198  footex  29201  tgaaddcpbllem1  29354  cgraer  29382  cgrabasimass  29383  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  prlngmolem2  29436  f1otrg  29453  2ndresdju  33290  rloccring  33878  qsdrngi  34065  1arithidom  34115  constrfin  34424