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 396   ∧ 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 397  df-3an 1089

This theorem is referenced by:  oppccatid  17615  subccatid  17746  fuccatid  17872  setccatid  17984  catccatid  18006  estrccatid  18033  xpccatid  18090  nllyidm  22877  utoptop  23623  cgr3tr4  34713  seglecgr12im  34771  paddasslem9  38364  cdlemd1  38734  cdlemf2  39098  cdlemk34  39446  dihmeetlem18N  39860  dihmeetlem19N  39861  isthincd2  47178  mndtccatid  47233