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 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  17620  subccatid  17748  fuccatid  17874  setccatid  17986  catccatid  18008  estrccatid  18033  xpccatid  18089  nllyidm  23399  utoptop  24144  cgr3tr4  36086  paddasslem9  39867  cdlemd1  40237  cdlemf2  40601  cdlemk34  40949  dihmeetlem18N  41363  dihmeetlem19N  41364  ssccatid  49104  isthincd2  49469  mndtccatid  49619