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 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  poxp2  8124  oppccatid  17661  subccatid  17792  setccatid  18030  catccatid  18052  estrccatid  18079  xpccatid  18136  gsmsymgreqlem1  19291  dmdprdsplit  19909  neitr  22666  neitx  23093  tx1stc  23136  utop3cls  23738  metustsym  24046  clwwlkccat  29223  3pthdlem1  29397  archiabllem1  32317  esumpcvgval  33014  esum2d  33029  ifscgr  34954  btwnconn1lem8  35004  btwnconn1lem11  35007  btwnconn1lem12  35008  segletr  35024  broutsideof3  35036  unbdqndv2  35325  lhp2lt  38810  cdlemf2  39371  cdlemn11pre  40019  stoweidlem60  44711  isthincd2  47560  mndtccatid  47615