Theorem simpr1r 1250

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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 402  df-3an 1105

This theorem is used by:  poxp2  8148  oppccatid  17800  subccatid  17928  setccatid  18166  catccatid  18188  estrccatid  18213  xpccatid  18269  gsmsymgreqlem1  19531  dmdprdsplit  20150  neitr  23374  neitx  23801  tx1stc  23844  utop3cls  24445  metustsym  24749  clwwlkccat  30378  3pthdlem1  30552  archiabllem1  33544  esumpcvgval  34499  esum2d  34514  ifscgr  36557  btwnconn1lem8  36607  btwnconn1lem11  36610  btwnconn1lem12  36611  segletr  36627  broutsideof3  36639  unbdqndv2  37141  lhp2lt  40816  cdlemf2  41377  cdlemn11pre  42025  stoweidlem60  46815  ssccatid  49891  isthincd2  50256  mndtccatid  50406