Theorem simpr1l 1232

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8095  poxp3  8102  oppccatid  17654  subccatid  17782  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  gsmsymgreqlem1  19371  dmdprdsplit  19990  neiptopnei  23088  neitr  23136  neitx  23563  tx1stc  23606  utop3cls  24207  metustsym  24511  ax5seg  29023  clwwlkccat  30077  3pthdlem1  30251  esumpcvgval  34255  esum2d  34270  ifscgr  36257  brofs2  36290  brifs2  36291  btwnconn1lem8  36307  btwnconn1lem12  36311  seglecgr12im  36323  unbdqndv2  36730  lhp2lt  40371  cdlemd1  40568  cdleme3b  40599  cdleme3c  40600  cdleme3e  40602  cdlemf2  40932  cdlemg4c  40982  cdlemn11pre  41580  dihmeetlem12N  41688  stoweidlem60  46412  ssccatid  49425  isthincd2  49790  mndtccatid  49940