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 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  17762  subccatid  17891  fuccatid  18017  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  nllyidm  23497  utoptop  24243  cgr3tr4  36053  seglecgr12im  36111  paddasslem9  39830  cdlemd1  40200  cdlemf2  40564  cdlemk34  40912  dihmeetlem18N  41326  dihmeetlem19N  41327  isthincd2  49086  mndtccatid  49184