Theorem simpr33 1284

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  oppccatid  17793  subccatid  17921  fuccatid  18047  setccatid  18159  catccatid  18181  estrccatid  18206  xpccatid  18262  nllyidm  23677  utoptop  24422  cgr3tr4  36557  paddasslem9  40635  cdlemd1  41005  cdlemf2  41369  cdlemk34  41717  dihmeetlem18N  42131  dihmeetlem19N  42132  ssccatid  49883  isthincd2  50248  mndtccatid  50398