Description: Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | simp-12l | ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ 𝜈 ) → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) | |
| 2 | 1 | ad11antr | ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ 𝜈 ) → 𝜑 ) |