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  8187  poxp3  8194  oppccatid  17922  subccatid  18050  setccatid  18288  catccatid  18310  estrccatid  18335  xpccatid  18391  gsmsymgreqlem1  19674  dmdprdsplit  20293  neiptopnei  23480  neitr  23528  neitx  23956  tx1stc  23999  utop3cls  24600  metustsym  24904  ax5seg  29546  clwwlkccat  30611  3pthdlem1  30795  esumpcvgval  34780  esum2d  34795  ifscgr  36987  brofs2  37020  brifs2  37021  btwnconn1lem8  37037  btwnconn1lem12  37041  seglecgr12im  37053  unbdqndv2  37555  lhp2lt  41250  cdlemd1  41447  cdleme3b  41478  cdleme3c  41479  cdleme3e  41481  cdlemf2  41811  cdlemg4c  41861  cdlemn11pre  42459  dihmeetlem12N  42567  stoweidlem60  47275  ssccatid  50391  isthincd2  50777  mndtccatid  50930