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  17685  subccatid  17813  fuccatid  17939  setccatid  18051  catccatid  18073  estrccatid  18098  xpccatid  18154  nllyidm  23454  utoptop  24199  cgr3tr4  36234  seglecgr12im  36292  paddasslem9  40274  cdlemd1  40644  cdlemf2  41008  cdlemk34  41356  dihmeetlem18N  41770  dihmeetlem19N  41771  ssccatid  49547  isthincd2  49912  mndtccatid  50062