Theorem simpr1r 1248

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 1205	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp2  8127  oppccatid  17765  subccatid  17893  setccatid  18131  catccatid  18153  estrccatid  18178  xpccatid  18234  gsmsymgreqlem1  19491  dmdprdsplit  20110  neitr  23298  neitx  23725  tx1stc  23768  utop3cls  24369  metustsym  24673  clwwlkccat  30250  3pthdlem1  30424  archiabllem1  33426  esumpcvgval  34385  esum2d  34400  ifscgr  36407  btwnconn1lem8  36457  btwnconn1lem11  36460  btwnconn1lem12  36461  segletr  36477  broutsideof3  36489  unbdqndv2  36962  lhp2lt  40637  cdlemf2  41198  cdlemn11pre  41846  stoweidlem60  46632  ssccatid  49701  isthincd2  50066  mndtccatid  50216