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  8085  oppccatid  17642  subccatid  17770  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  gsmsymgreqlem1  19359  dmdprdsplit  19978  neitr  23124  neitx  23551  tx1stc  23594  utop3cls  24195  metustsym  24499  clwwlkccat  30065  3pthdlem1  30239  archiabllem1  33275  esumpcvgval  34235  esum2d  34250  ifscgr  36238  btwnconn1lem8  36288  btwnconn1lem11  36291  btwnconn1lem12  36292  segletr  36308  broutsideof3  36320  unbdqndv2  36711  lhp2lt  40257  cdlemf2  40818  cdlemn11pre  41466  stoweidlem60  46300  ssccatid  49313  isthincd2  49678  mndtccatid  49828