Theorem simpr1r 1250

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr1r	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1r

Step	Hyp	Ref	Expression
1		simprr 785	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2antr1 1207	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8162  oppccatid  17898  subccatid  18026  setccatid  18264  catccatid  18286  estrccatid  18311  xpccatid  18367  gsmsymgreqlem1  19649  dmdprdsplit  20268  neitr  23503  neitx  23931  tx1stc  23974  utop3cls  24575  metustsym  24879  clwwlkccat  30586  3pthdlem1  30770  archiabllem1  33800  esumpcvgval  34756  esum2d  34771  ifscgr  36901  btwnconn1lem8  36951  btwnconn1lem11  36954  btwnconn1lem12  36955  segletr  36971  broutsideof3  36983  unbdqndv2  37469  lhp2lt  41151  cdlemf2  41712  cdlemn11pre  42360  stoweidlem60  47163  ssccatid  50279  isthincd2  50665  mndtccatid  50818