Theorem simpr31 1265

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  oppccatid  17654  subccatid  17782  fuccatid  17908  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  nllyidm  23445  utoptop  24190  cgr3tr4  36265  seglecgr12im  36323  paddasslem9  40198  cdlemd1  40568  cdlemf2  40932  cdlemk34  41280  dihmeetlem18N  41694  dihmeetlem19N  41695  ssccatid  49425  isthincd2  49790  mndtccatid  49940