Theorem simpr1r 1249

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  poxp2  8137  oppccatid  17781  subccatid  17909  setccatid  18147  catccatid  18169  estrccatid  18194  xpccatid  18250  gsmsymgreqlem1  19506  dmdprdsplit  20125  neitr  23348  neitx  23775  tx1stc  23818  utop3cls  24419  metustsym  24723  clwwlkccat  30352  3pthdlem1  30526  archiabllem1  33522  esumpcvgval  34477  esum2d  34492  ifscgr  36544  btwnconn1lem8  36594  btwnconn1lem11  36597  btwnconn1lem12  36598  segletr  36614  broutsideof3  36626  unbdqndv2  37128  lhp2lt  40803  cdlemf2  41364  cdlemn11pre  42012  stoweidlem60  46802  ssccatid  49878  isthincd2  50243  mndtccatid  50393