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  17676  subccatid  17804  fuccatid  17930  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  nllyidm  23464  utoptop  24209  cgr3tr4  36250  seglecgr12im  36308  paddasslem9  40288  cdlemd1  40658  cdlemf2  41022  cdlemk34  41370  dihmeetlem18N  41784  dihmeetlem19N  41785  ssccatid  49559  isthincd2  49924  mndtccatid  50074