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 1086

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 1088

This theorem is referenced by:  oppccatid  17731  subccatid  17859  fuccatid  17985  setccatid  18097  catccatid  18119  estrccatid  18144  xpccatid  18200  nllyidm  23427  utoptop  24173  cgr3tr4  36070  seglecgr12im  36128  paddasslem9  39847  cdlemd1  40217  cdlemf2  40581  cdlemk34  40929  dihmeetlem18N  41343  dihmeetlem19N  41344  ssccatid  49039  isthincd2  49323  mndtccatid  49464