Theorem simpr1r 1227

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oppccatid  16989  subccatid  17116  setccatid  17344  catccatid  17362  estrccatid  17382  xpccatid  17438  gsmsymgreqlem1  18558  dmdprdsplit  19169  neitr  21788  neitx  22215  tx1stc  22258  utop3cls  22860  metustsym  23165  clwwlkccat  27768  3pthdlem1  27943  archiabllem1  30822  esumpcvgval  31337  esum2d  31352  ifscgr  33505  btwnconn1lem8  33555  btwnconn1lem11  33558  btwnconn1lem12  33559  segletr  33575  broutsideof3  33587  unbdqndv2  33850  lhp2lt  37152  cdlemf2  37713  cdlemn11pre  38361  stoweidlem60  42365