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  8148  poxp3  8155  oppccatid  17800  subccatid  17928  setccatid  18166  catccatid  18188  estrccatid  18213  xpccatid  18269  gsmsymgreqlem1  19531  dmdprdsplit  20150  neiptopnei  23326  neitr  23374  neitx  23801  tx1stc  23844  utop3cls  24445  metustsym  24749  ax5seg  29325  clwwlkccat  30378  3pthdlem1  30552  esumpcvgval  34499  esum2d  34514  ifscgr  36557  brofs2  36590  brifs2  36591  btwnconn1lem8  36607  btwnconn1lem12  36611  seglecgr12im  36623  unbdqndv2  37141  lhp2lt  40816  cdlemd1  41013  cdleme3b  41044  cdleme3c  41045  cdleme3e  41047  cdlemf2  41377  cdlemg4c  41427  cdlemn11pre  42025  dihmeetlem12N  42133  stoweidlem60  46815  ssccatid  49891  isthincd2  50256  mndtccatid  50406