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  8073  poxp3  8080  oppccatid  17622  subccatid  17750  setccatid  17988  catccatid  18010  estrccatid  18035  xpccatid  18091  gsmsymgreqlem1  19340  dmdprdsplit  19959  neiptopnei  23045  neitr  23093  neitx  23520  tx1stc  23563  utop3cls  24164  metustsym  24468  ax5seg  28914  clwwlkccat  29965  3pthdlem1  30139  esumpcvgval  34086  esum2d  34101  ifscgr  36077  brofs2  36110  brifs2  36111  btwnconn1lem8  36127  btwnconn1lem12  36131  seglecgr12im  36143  unbdqndv2  36544  lhp2lt  40039  cdlemd1  40236  cdleme3b  40267  cdleme3c  40268  cdleme3e  40270  cdlemf2  40600  cdlemg4c  40650  cdlemn11pre  41248  dihmeetlem12N  41356  stoweidlem60  46097  ssccatid  49103  isthincd2  49468  mndtccatid  49618