Theorem simpr32 1283

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  oppccatid  17776  subccatid  17904  fuccatid  18030  setccatid  18142  catccatid  18164  estrccatid  18189  xpccatid  18245  omndmul2  20204  nllyidm  23627  utoptop  24372  cgr3tr4  36522  paddasslem9  40580  cdlemd1  40950  cdlemf2  41314  cdlemk34  41662  dihmeetlem18N  42076  ssccatid  49827  isthincd2  50192  mndtccatid  50342