Theorem simpr1r 1232

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 772	. 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  8079  oppccatid  17627  subccatid  17755  setccatid  17993  catccatid  18015  estrccatid  18040  xpccatid  18096  gsmsymgreqlem1  19344  dmdprdsplit  19963  neitr  23096  neitx  23523  tx1stc  23566  utop3cls  24167  metustsym  24471  clwwlkccat  29972  3pthdlem1  30146  archiabllem1  33169  esumpcvgval  34112  esum2d  34127  ifscgr  36109  btwnconn1lem8  36159  btwnconn1lem11  36162  btwnconn1lem12  36163  segletr  36179  broutsideof3  36191  unbdqndv2  36576  lhp2lt  40120  cdlemf2  40681  cdlemn11pre  41329  stoweidlem60  46182  ssccatid  49197  isthincd2  49562  mndtccatid  49712