Theorem simpr31 1264

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

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

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 1088

This theorem is referenced by:  oppccatid  17642  subccatid  17770  fuccatid  17896  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  nllyidm  23433  utoptop  24178  cgr3tr4  36246  seglecgr12im  36304  paddasslem9  40084  cdlemd1  40454  cdlemf2  40818  cdlemk34  41166  dihmeetlem18N  41580  dihmeetlem19N  41581  ssccatid  49313  isthincd2  49678  mndtccatid  49828