Theorem simpr1r 1233

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 1190	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  8086  oppccatid  17676  subccatid  17804  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  gsmsymgreqlem1  19396  dmdprdsplit  20015  neitr  23155  neitx  23582  tx1stc  23625  utop3cls  24226  metustsym  24530  clwwlkccat  30075  3pthdlem1  30249  archiabllem1  33269  esumpcvgval  34238  esum2d  34253  ifscgr  36242  btwnconn1lem8  36292  btwnconn1lem11  36295  btwnconn1lem12  36296  segletr  36312  broutsideof3  36324  unbdqndv2  36787  lhp2lt  40461  cdlemf2  41022  cdlemn11pre  41670  stoweidlem60  46506  ssccatid  49559  isthincd2  49924  mndtccatid  50074