Theorem simpr31 1260

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  oppccatid  17755  subccatid  17886  fuccatid  18015  setccatid  18127  catccatid  18149  estrccatid  18176  xpccatid  18233  nllyidm  23507  utoptop  24253  cgr3tr4  35923  seglecgr12im  35981  paddasslem9  39574  cdlemd1  39944  cdlemf2  40308  cdlemk34  40656  dihmeetlem18N  41070  dihmeetlem19N  41071  isthincd2  48440  mndtccatid  48495