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  8085  poxp3  8092  oppccatid  17642  subccatid  17770  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  gsmsymgreqlem1  19359  dmdprdsplit  19978  neiptopnei  23076  neitr  23124  neitx  23551  tx1stc  23594  utop3cls  24195  metustsym  24499  ax5seg  29011  clwwlkccat  30065  3pthdlem1  30239  esumpcvgval  34235  esum2d  34250  ifscgr  36238  brofs2  36271  brifs2  36272  btwnconn1lem8  36288  btwnconn1lem12  36292  seglecgr12im  36304  unbdqndv2  36711  lhp2lt  40257  cdlemd1  40454  cdleme3b  40485  cdleme3c  40486  cdleme3e  40488  cdlemf2  40818  cdlemg4c  40868  cdlemn11pre  41466  dihmeetlem12N  41574  stoweidlem60  46300  ssccatid  49313  isthincd2  49678  mndtccatid  49828