Theorem simpr1l 1231

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr1l	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr1l

Step	Hyp	Ref	Expression
1		simprl 770	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 1189	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:  poxp2  8079  poxp3  8086  oppccatid  17627  subccatid  17755  setccatid  17993  catccatid  18015  estrccatid  18040  xpccatid  18096  gsmsymgreqlem1  19344  dmdprdsplit  19963  neiptopnei  23048  neitr  23096  neitx  23523  tx1stc  23566  utop3cls  24167  metustsym  24471  ax5seg  28918  clwwlkccat  29972  3pthdlem1  30146  esumpcvgval  34112  esum2d  34127  ifscgr  36109  brofs2  36142  brifs2  36143  btwnconn1lem8  36159  btwnconn1lem12  36163  seglecgr12im  36175  unbdqndv2  36576  lhp2lt  40120  cdlemd1  40317  cdleme3b  40348  cdleme3c  40349  cdleme3e  40351  cdlemf2  40681  cdlemg4c  40731  cdlemn11pre  41329  dihmeetlem12N  41437  stoweidlem60  46182  ssccatid  49197  isthincd2  49562  mndtccatid  49712