Theorem simpr32 1271

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

Assertion

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

Proof of Theorem simpr32

Step	Hyp	Ref	Expression
1		simpr2 1202	. 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	3ad2antr3 1197	1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

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

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  oppccatid  17683  subccatid  17811  fuccatid  17937  setccatid  18049  catccatid  18071  estrccatid  18096  xpccatid  18152  omndmul2  20106  nllyidm  23479  utoptop  24224  cgr3tr4  36287  paddasslem9  40327  cdlemd1  40697  cdlemf2  41061  cdlemk34  41409  dihmeetlem18N  41823  ssccatid  49569  isthincd2  49934  mndtccatid  50084