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  8145  oppccatid  17813  subccatid  17941  setccatid  18179  catccatid  18201  estrccatid  18226  xpccatid  18282  gsmsymgreqlem1  19563  dmdprdsplit  20182  neitr  23411  neitx  23839  tx1stc  23882  utop3cls  24483  metustsym  24787  clwwlkccat  30468  3pthdlem1  30652  archiabllem1  33641  esumpcvgval  34596  esum2d  34611  ifscgr  36632  btwnconn1lem8  36682  btwnconn1lem11  36685  btwnconn1lem12  36686  segletr  36702  broutsideof3  36714  unbdqndv2  37216  lhp2lt  40882  cdlemf2  41443  cdlemn11pre  42091  stoweidlem60  46896  ssccatid  50006  isthincd2  50371  mndtccatid  50521