Theorem simpr32 1265

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  oppccatid  17643  subccatid  17771  fuccatid  17897  setccatid  18009  catccatid  18031  estrccatid  18056  xpccatid  18112  omndmul2  20030  nllyidm  23392  utoptop  24138  cgr3tr4  36025  paddasslem9  39807  cdlemd1  40177  cdlemf2  40541  cdlemk34  40889  dihmeetlem18N  41303  ssccatid  49058  isthincd2  49423  mndtccatid  49573