Theorem simpr1r 1232

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8168  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  gsmsymgreqlem1  19448  dmdprdsplit  20067  neitr  23188  neitx  23615  tx1stc  23658  utop3cls  24260  metustsym  24568  clwwlkccat  30009  3pthdlem1  30183  archiabllem1  33200  esumpcvgval  34079  esum2d  34094  ifscgr  36045  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  segletr  36115  broutsideof3  36127  unbdqndv2  36512  lhp2lt  40003  cdlemf2  40564  cdlemn11pre  41212  stoweidlem60  46075  isthincd2  49086  mndtccatid  49184