Theorem simpr1l 1291

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  oppccatid  16580  subccatid  16707  setccatid  16935  catccatid  16953  estrccatid  16973  xpccatid  17029  gsmsymgreqlem1  18050  dmdprdsplit  18646  neiptopnei  21138  neitr  21186  neitx  21612  tx1stc  21655  utop3cls  22256  metustsym  22561  ax5seg  26017  3pthdlem1  27316  esumpcvgval  30449  esum2d  30464  ifscgr  32457  brofs2  32490  brifs2  32491  btwnconn1lem8  32507  btwnconn1lem12  32511  seglecgr12im  32523  unbdqndv2  32808  lhp2lt  35790  cdlemd1  35988  cdleme3b  36019  cdleme3c  36020  cdleme3e  36022  cdlemf2  36352  cdlemg4c  36402  cdlemn11pre  37001  dihmeetlem12N  37109  stoweidlem60  40780