Theorem simpr31 1261

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  oppccatid  17411  subccatid  17542  fuccatid  17668  setccatid  17780  catccatid  17802  estrccatid  17829  xpccatid  17886  nllyidm  22621  utoptop  23367  cgr3tr4  34333  seglecgr12im  34391  paddasslem9  37821  cdlemd1  38191  cdlemf2  38555  cdlemk34  38903  dihmeetlem18N  39317  dihmeetlem19N  39318  isthincd2  46271  mndtccatid  46326