Theorem simpr31 1282

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  oppccatid  17813  subccatid  17941  fuccatid  18067  setccatid  18179  catccatid  18201  estrccatid  18226  xpccatid  18282  nllyidm  23721  utoptop  24466  cgr3tr4  36640  seglecgr12im  36698  paddasslem9  40709  cdlemd1  41079  cdlemf2  41443  cdlemk34  41791  dihmeetlem18N  42205  dihmeetlem19N  42206  ssccatid  50006  isthincd2  50371  mndtccatid  50521