Theorem simpr1l 1226

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oppccatid  16989  subccatid  17116  setccatid  17344  catccatid  17362  estrccatid  17382  xpccatid  17438  gsmsymgreqlem1  18558  dmdprdsplit  19169  neiptopnei  21740  neitr  21788  neitx  22215  tx1stc  22258  utop3cls  22860  metustsym  23165  ax5seg  26724  clwwlkccat  27768  3pthdlem1  27943  esumpcvgval  31337  esum2d  31352  ifscgr  33505  brofs2  33538  brifs2  33539  btwnconn1lem8  33555  btwnconn1lem12  33559  seglecgr12im  33571  unbdqndv2  33850  lhp2lt  37152  cdlemd1  37349  cdleme3b  37380  cdleme3c  37381  cdleme3e  37383  cdlemf2  37713  cdlemg4c  37763  cdlemn11pre  38361  dihmeetlem12N  38469  stoweidlem60  42365