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  17686  subccatid  17814  fuccatid  17940  setccatid  18052  catccatid  18074  estrccatid  18099  xpccatid  18155  nllyidm  23382  utoptop  24128  cgr3tr4  36035  paddasslem9  39817  cdlemd1  40187  cdlemf2  40551  cdlemk34  40899  dihmeetlem18N  41313  dihmeetlem19N  41314  ssccatid  49051  isthincd2  49416  mndtccatid  49566