Theorem simpr1r 1307

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1107

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 198  df-an 385  df-3an 1109

This theorem is referenced by:  oppccatid  16647  subccatid  16774  setccatid  17002  catccatid  17020  estrccatid  17040  xpccatid  17097  gsmsymgreqlem1  18116  dmdprdsplit  18716  neitr  21267  neitx  21693  tx1stc  21736  utop3cls  22337  metustsym  22642  clwwlkccat  27220  3pthdlem1  27445  archiabllem1  30197  esumpcvgval  30590  esum2d  30605  ifscgr  32598  btwnconn1lem8  32648  btwnconn1lem11  32651  btwnconn1lem12  32652  segletr  32668  broutsideof3  32680  unbdqndv2  32944  lhp2lt  35960  cdlemf2  36521  cdlemn11pre  37169  stoweidlem60  40917