Theorem simpr31 1282

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr31	⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Proof of Theorem simpr31

Step	Hyp	Ref	Expression
1		simpr1 1213	. 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  17922  subccatid  18050  fuccatid  18176  setccatid  18288  catccatid  18310  estrccatid  18335  xpccatid  18391  nllyidm  23838  utoptop  24583  cgr3tr4  36995  seglecgr12im  37053  paddasslem9  41077  cdlemd1  41447  cdlemf2  41811  cdlemk34  42159  dihmeetlem18N  42573  dihmeetlem19N  42574  ssccatid  50391  isthincd2  50777  mndtccatid  50930