Theorem simpr1r 1228

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 1185	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  oppccatid  16981  subccatid  17108  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  gsmsymgreqlem1  18550  dmdprdsplit  19162  neitr  21785  neitx  22212  tx1stc  22255  utop3cls  22857  metustsym  23162  clwwlkccat  27775  3pthdlem1  27949  archiabllem1  30872  esumpcvgval  31447  esum2d  31462  ifscgr  33618  btwnconn1lem8  33668  btwnconn1lem11  33671  btwnconn1lem12  33672  segletr  33688  broutsideof3  33700  unbdqndv2  33963  lhp2lt  37297  cdlemf2  37858  cdlemn11pre  38506  stoweidlem60  42702