Theorem simpr1r 1292

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  oppccatid  16587  subccatid  16714  setccatid  16942  catccatid  16960  estrccatid  16980  xpccatid  17037  gsmsymgreqlem1  18058  dmdprdsplit  18655  neitr  21206  neitx  21632  tx1stc  21675  utop3cls  22276  metustsym  22581  clwwlkccat  27141  3pthdlem1  27345  archiabllem1  30088  esumpcvgval  30481  esum2d  30496  ifscgr  32489  btwnconn1lem8  32539  btwnconn1lem11  32542  btwnconn1lem12  32543  segletr  32559  broutsideof3  32571  unbdqndv2  32840  lhp2lt  35810  cdlemf2  36372  cdlemn11pre  37021  stoweidlem60  40795