Theorem simpr33 1282

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 1103

This theorem is referenced by:  oppccatid  17771  subccatid  17899  fuccatid  18025  setccatid  18137  catccatid  18159  estrccatid  18184  xpccatid  18240  nllyidm  23611  utoptop  24356  cgr3tr4  36439  paddasslem9  40487  cdlemd1  40857  cdlemf2  41221  cdlemk34  41569  dihmeetlem18N  41983  dihmeetlem19N  41984  ssccatid  49728  isthincd2  50093  mndtccatid  50243