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  8073  oppccatid  17622  subccatid  17750  setccatid  17988  catccatid  18010  estrccatid  18035  xpccatid  18091  gsmsymgreqlem1  19340  dmdprdsplit  19959  neitr  23093  neitx  23520  tx1stc  23563  utop3cls  24164  metustsym  24468  clwwlkccat  29965  3pthdlem1  30139  archiabllem1  33157  esumpcvgval  34086  esum2d  34101  ifscgr  36077  btwnconn1lem8  36127  btwnconn1lem11  36130  btwnconn1lem12  36131  segletr  36147  broutsideof3  36159  unbdqndv2  36544  lhp2lt  40039  cdlemf2  40600  cdlemn11pre  41248  stoweidlem60  46097  ssccatid  49103  isthincd2  49468  mndtccatid  49618