Theorem simpr1r 1233

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 773	. 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  oppccatid  17654  subccatid  17782  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  gsmsymgreqlem1  19371  dmdprdsplit  19990  neitr  23136  neitx  23563  tx1stc  23606  utop3cls  24207  metustsym  24511  clwwlkccat  30077  3pthdlem1  30251  archiabllem1  33286  esumpcvgval  34255  esum2d  34270  ifscgr  36257  btwnconn1lem8  36307  btwnconn1lem11  36310  btwnconn1lem12  36311  segletr  36327  broutsideof3  36339  unbdqndv2  36730  lhp2lt  40371  cdlemf2  40932  cdlemn11pre  41580  stoweidlem60  46412  ssccatid  49425  isthincd2  49790  mndtccatid  49940