Theorem simpr1l 1231

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

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

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 1088

This theorem is referenced by:  poxp2  8125  poxp3  8132  oppccatid  17687  subccatid  17815  setccatid  18053  catccatid  18075  estrccatid  18100  xpccatid  18156  gsmsymgreqlem1  19367  dmdprdsplit  19986  neiptopnei  23026  neitr  23074  neitx  23501  tx1stc  23544  utop3cls  24146  metustsym  24450  ax5seg  28872  clwwlkccat  29926  3pthdlem1  30100  esumpcvgval  34075  esum2d  34090  ifscgr  36039  brofs2  36072  brifs2  36073  btwnconn1lem8  36089  btwnconn1lem12  36093  seglecgr12im  36105  unbdqndv2  36506  lhp2lt  40002  cdlemd1  40199  cdleme3b  40230  cdleme3c  40231  cdleme3e  40233  cdlemf2  40563  cdlemg4c  40613  cdlemn11pre  41211  dihmeetlem12N  41319  stoweidlem60  46065  ssccatid  49065  isthincd2  49430  mndtccatid  49580