Theorem simpr31 1263

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  oppccatid  17475  subccatid  17606  fuccatid  17732  setccatid  17844  catccatid  17866  estrccatid  17893  xpccatid  17950  nllyidm  22685  utoptop  23431  cgr3tr4  34399  seglecgr12im  34457  paddasslem9  37884  cdlemd1  38254  cdlemf2  38618  cdlemk34  38966  dihmeetlem18N  39380  dihmeetlem19N  39381  isthincd2  46377  mndtccatid  46432