Theorem simpr31 1282

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr31	⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Proof of Theorem simpr31

Step	Hyp	Ref	Expression
1		simpr1 1213	. 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	3ad2antr3 1209	1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  oppccatid  17800  subccatid  17928  fuccatid  18054  setccatid  18166  catccatid  18188  estrccatid  18213  xpccatid  18269  nllyidm  23683  utoptop  24428  cgr3tr4  36565  seglecgr12im  36623  paddasslem9  40643  cdlemd1  41013  cdlemf2  41377  cdlemk34  41725  dihmeetlem18N  42139  dihmeetlem19N  42140  ssccatid  49891  isthincd2  50256  mndtccatid  50406