Theorem simpr32 1262

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  oppccatid  17669  subccatid  17800  fuccatid  17926  setccatid  18038  catccatid  18060  estrccatid  18087  xpccatid  18144  nllyidm  23213  utoptop  23959  omndmul2  32500  cgr3tr4  35328  paddasslem9  39002  cdlemd1  39372  cdlemf2  39736  cdlemk34  40084  dihmeetlem18N  40498  isthincd2  47745  mndtccatid  47800