Theorem simpr31 1262

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 1193	. 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	3ad2antr3 1189	1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  oppccatid  17527  subccatid  17658  fuccatid  17784  setccatid  17896  catccatid  17918  estrccatid  17945  xpccatid  18002  nllyidm  22746  utoptop  23492  cgr3tr4  34450  seglecgr12im  34508  paddasslem9  38104  cdlemd1  38474  cdlemf2  38838  cdlemk34  39186  dihmeetlem18N  39600  dihmeetlem19N  39601  isthincd2  46678  mndtccatid  46733