Theorem simpr33 1266

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

Assertion

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

Proof of Theorem simpr33

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  oppccatid  17775  subccatid  17906  fuccatid  18035  setccatid  18147  catccatid  18169  estrccatid  18196  xpccatid  18253  nllyidm  23522  utoptop  24268  cgr3tr4  36047  paddasslem9  39825  cdlemd1  40195  cdlemf2  40559  cdlemk34  40907  dihmeetlem18N  41321  dihmeetlem19N  41322  isthincd2  48963  mndtccatid  49021