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 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

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  17770  subccatid  17898  fuccatid  18024  setccatid  18136  catccatid  18158  estrccatid  18183  xpccatid  18239  nllyidm  23646  utoptop  24391  cgr3tr4  36544  paddasslem9  40602  cdlemd1  40972  cdlemf2  41336  cdlemk34  41684  dihmeetlem18N  42098  dihmeetlem19N  42099  ssccatid  49850  isthincd2  50215  mndtccatid  50365