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  8125  oppccatid  17687  subccatid  17815  setccatid  18053  catccatid  18075  estrccatid  18100  xpccatid  18156  gsmsymgreqlem1  19367  dmdprdsplit  19986  neitr  23074  neitx  23501  tx1stc  23544  utop3cls  24146  metustsym  24450  clwwlkccat  29926  3pthdlem1  30100  archiabllem1  33154  esumpcvgval  34075  esum2d  34090  ifscgr  36039  btwnconn1lem8  36089  btwnconn1lem11  36092  btwnconn1lem12  36093  segletr  36109  broutsideof3  36121  unbdqndv2  36506  lhp2lt  40002  cdlemf2  40563  cdlemn11pre  41211  stoweidlem60  46065  ssccatid  49065  isthincd2  49430  mndtccatid  49580