Theorem simpr1l 1237

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 776	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 1195	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  poxp3  8097  oppccatid  17683  subccatid  17811  setccatid  18049  catccatid  18071  estrccatid  18096  xpccatid  18152  gsmsymgreqlem1  19403  dmdprdsplit  20022  neiptopnei  23122  neitr  23170  neitx  23597  tx1stc  23640  utop3cls  24241  metustsym  24545  ax5seg  29032  clwwlkccat  30085  3pthdlem1  30259  esumpcvgval  34269  esum2d  34284  ifscgr  36279  brofs2  36312  brifs2  36313  btwnconn1lem8  36329  btwnconn1lem12  36333  seglecgr12im  36345  unbdqndv2  36824  lhp2lt  40500  cdlemd1  40697  cdleme3b  40728  cdleme3c  40729  cdleme3e  40731  cdlemf2  41061  cdlemg4c  41111  cdlemn11pre  41709  dihmeetlem12N  41817  stoweidlem60  46510  ssccatid  49569  isthincd2  49934  mndtccatid  50084