Theorem simpr33 1278

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  oppccatid  17742  subccatid  17870  fuccatid  17996  setccatid  18108  catccatid  18130  estrccatid  18155  xpccatid  18211  nllyidm  23537  utoptop  24282  cgr3tr4  36363  paddasslem9  40413  cdlemd1  40783  cdlemf2  41147  cdlemk34  41495  dihmeetlem18N  41909  dihmeetlem19N  41910  ssccatid  49654  isthincd2  50019  mndtccatid  50169