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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 206  df-an 396  df-3an 1086

This theorem is referenced by:  poxp2  8124  poxp3  8131  oppccatid  17666  subccatid  17797  setccatid  18038  catccatid  18060  estrccatid  18087  xpccatid  18144  gsmsymgreqlem1  19342  dmdprdsplit  19961  neiptopnei  22960  neitr  23008  neitx  23435  tx1stc  23478  utop3cls  24080  metustsym  24388  ax5seg  28668  clwwlkccat  29715  3pthdlem1  29889  esumpcvgval  33568  esum2d  33583  ifscgr  35512  brofs2  35545  brifs2  35546  btwnconn1lem8  35562  btwnconn1lem12  35566  seglecgr12im  35578  unbdqndv2  35878  lhp2lt  39366  cdlemd1  39563  cdleme3b  39594  cdleme3c  39595  cdleme3e  39597  cdlemf2  39927  cdlemg4c  39977  cdlemn11pre  40575  dihmeetlem12N  40683  stoweidlem60  45286  isthincd2  47870  mndtccatid  47925