Theorem simpr1l 1227

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 1185	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  oppccatid  16981  subccatid  17108  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  gsmsymgreqlem1  18550  dmdprdsplit  19162  neiptopnei  21737  neitr  21785  neitx  22212  tx1stc  22255  utop3cls  22857  metustsym  23162  ax5seg  26732  clwwlkccat  27775  3pthdlem1  27949  esumpcvgval  31447  esum2d  31462  ifscgr  33618  brofs2  33651  brifs2  33652  btwnconn1lem8  33668  btwnconn1lem12  33672  seglecgr12im  33684  unbdqndv2  33963  lhp2lt  37297  cdlemd1  37494  cdleme3b  37525  cdleme3c  37526  cdleme3e  37528  cdlemf2  37858  cdlemg4c  37908  cdlemn11pre  38506  dihmeetlem12N  38614  stoweidlem60  42702