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  8187  oppccatid  17922  subccatid  18050  setccatid  18288  catccatid  18310  estrccatid  18335  xpccatid  18391  gsmsymgreqlem1  19674  dmdprdsplit  20293  neitr  23528  neitx  23956  tx1stc  23999  utop3cls  24600  metustsym  24904  clwwlkccat  30611  3pthdlem1  30795  archiabllem1  33824  esumpcvgval  34780  esum2d  34795  ifscgr  36987  btwnconn1lem8  37037  btwnconn1lem11  37040  btwnconn1lem12  37041  segletr  37057  broutsideof3  37069  unbdqndv2  37555  lhp2lt  41250  cdlemf2  41811  cdlemn11pre  42459  stoweidlem60  47275  ssccatid  50391  isthincd2  50777  mndtccatid  50930