Theorem simpr1l 1262

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  oppccatid  16764  subccatid  16891  setccatid  17119  catccatid  17137  estrccatid  17157  xpccatid  17214  gsmsymgreqlem1  18233  dmdprdsplit  18833  neiptopnei  21344  neitr  21392  neitx  21819  tx1stc  21862  utop3cls  22463  metustsym  22768  ax5seg  26287  3pthdlem1  27567  esumpcvgval  30738  esum2d  30753  ifscgr  32740  brofs2  32773  brifs2  32774  btwnconn1lem8  32790  btwnconn1lem12  32794  seglecgr12im  32806  unbdqndv2  33084  lhp2lt  36157  cdlemd1  36354  cdleme3b  36385  cdleme3c  36386  cdleme3e  36388  cdlemf2  36718  cdlemg4c  36768  cdlemn11pre  37366  dihmeetlem12N  37474  stoweidlem60  41208