Theorem simpr1r 1231

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

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

This theorem is referenced by:  poxp2  8128  oppccatid  17664  subccatid  17795  setccatid  18033  catccatid  18055  estrccatid  18082  xpccatid  18139  gsmsymgreqlem1  19297  dmdprdsplit  19916  neitr  22683  neitx  23110  tx1stc  23153  utop3cls  23755  metustsym  24063  clwwlkccat  29240  3pthdlem1  29414  archiabllem1  32334  esumpcvgval  33071  esum2d  33086  ifscgr  35011  btwnconn1lem8  35061  btwnconn1lem11  35064  btwnconn1lem12  35065  segletr  35081  broutsideof3  35093  unbdqndv2  35382  lhp2lt  38867  cdlemf2  39428  cdlemn11pre  40076  stoweidlem60  44766  isthincd2  47648  mndtccatid  47703