Theorem simpr31 1276

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  oppccatid  17734  subccatid  17862  fuccatid  17988  setccatid  18100  catccatid  18122  estrccatid  18147  xpccatid  18203  nllyidm  23529  utoptop  24274  cgr3tr4  36366  seglecgr12im  36424  paddasslem9  40416  cdlemd1  40786  cdlemf2  41150  cdlemk34  41498  dihmeetlem18N  41912  dihmeetlem19N  41913  ssccatid  49657  isthincd2  50022  mndtccatid  50172