Theorem simpr32 1264

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 1195	. 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  17661  subccatid  17792  fuccatid  17918  setccatid  18030  catccatid  18052  estrccatid  18079  xpccatid  18136  nllyidm  22984  utoptop  23730  omndmul2  32217  cgr3tr4  35012  paddasslem9  38687  cdlemd1  39057  cdlemf2  39421  cdlemk34  39769  dihmeetlem18N  40183  isthincd2  47611  mndtccatid  47666