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  17873  subccatid  18001  fuccatid  18127  setccatid  18239  catccatid  18261  estrccatid  18286  xpccatid  18342  nllyidm  23788  utoptop  24533  cgr3tr4  36787  seglecgr12im  36845  paddasslem9  40853  cdlemd1  41223  cdlemf2  41587  cdlemk34  41935  dihmeetlem18N  42349  dihmeetlem19N  42350  ssccatid  50124  isthincd2  50489  mndtccatid  50639