Theorem simpr1r 1225

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

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

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 1083

This theorem is referenced by:  oppccatid  16981  subccatid  17108  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  gsmsymgreqlem1  18550  dmdprdsplit  19161  neitr  21780  neitx  22207  tx1stc  22250  utop3cls  22852  metustsym  23157  clwwlkccat  27760  3pthdlem1  27935  archiabllem1  30815  esumpcvgval  31330  esum2d  31345  ifscgr  33498  btwnconn1lem8  33548  btwnconn1lem11  33551  btwnconn1lem12  33552  segletr  33568  broutsideof3  33580  unbdqndv2  33843  lhp2lt  37129  cdlemf2  37690  cdlemn11pre  38338  stoweidlem60  42335