Theorem simpr1l 1249

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 783	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 1207	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:  poxp2  8162  poxp3  8169  oppccatid  17898  subccatid  18026  setccatid  18264  catccatid  18286  estrccatid  18311  xpccatid  18367  gsmsymgreqlem1  19649  dmdprdsplit  20268  neiptopnei  23455  neitr  23503  neitx  23931  tx1stc  23974  utop3cls  24575  metustsym  24879  ax5seg  29521  clwwlkccat  30586  3pthdlem1  30770  esumpcvgval  34756  esum2d  34771  ifscgr  36901  brofs2  36934  brifs2  36935  btwnconn1lem8  36951  btwnconn1lem12  36955  seglecgr12im  36967  unbdqndv2  37469  lhp2lt  41151  cdlemd1  41348  cdleme3b  41379  cdleme3c  41380  cdleme3e  41382  cdlemf2  41712  cdlemg4c  41762  cdlemn11pre  42360  dihmeetlem12N  42468  stoweidlem60  47163  ssccatid  50279  isthincd2  50665  mndtccatid  50818