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  8145  poxp3  8152  oppccatid  17813  subccatid  17941  setccatid  18179  catccatid  18201  estrccatid  18226  xpccatid  18282  gsmsymgreqlem1  19563  dmdprdsplit  20182  neiptopnei  23363  neitr  23411  neitx  23839  tx1stc  23882  utop3cls  24483  metustsym  24787  ax5seg  29403  clwwlkccat  30468  3pthdlem1  30652  esumpcvgval  34596  esum2d  34611  ifscgr  36632  brofs2  36665  brifs2  36666  btwnconn1lem8  36682  btwnconn1lem12  36686  seglecgr12im  36698  unbdqndv2  37216  lhp2lt  40882  cdlemd1  41079  cdleme3b  41110  cdleme3c  41111  cdleme3e  41113  cdlemf2  41443  cdlemg4c  41493  cdlemn11pre  42091  dihmeetlem12N  42199  stoweidlem60  46896  ssccatid  50006  isthincd2  50371  mndtccatid  50521