Theorem simpr31 1280

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 1211	. 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  17765  subccatid  17893  fuccatid  18019  setccatid  18131  catccatid  18153  estrccatid  18178  xpccatid  18234  nllyidm  23607  utoptop  24352  cgr3tr4  36415  seglecgr12im  36473  paddasslem9  40464  cdlemd1  40834  cdlemf2  41198  cdlemk34  41546  dihmeetlem18N  41960  dihmeetlem19N  41961  ssccatid  49701  isthincd2  50066  mndtccatid  50216