Theorem simpr1r 1112

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpr1r	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1r

Step	Hyp	Ref	Expression
1		simp1r 1079	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	adantl 481	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  oppccatid  16202  subccatid  16329  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  gsmsymgreqlem1  17673  dmdprdsplit  18269  neitr  20794  neitx  21220  tx1stc  21263  utop3cls  21865  metustsym  22170  frgrawopreg  26576  archiabllem1  29078  esumpcvgval  29467  esum2d  29482  ifscgr  31321  btwnconn1lem8  31371  btwnconn1lem11  31374  btwnconn1lem12  31375  segletr  31391  broutsideof3  31403  unbdqndv2  31672  lhp2lt  34305  cdlemf2  34868  cdlemn11pre  35517  stoweidlem60  38953  3pthdlem1  41331  frgrwopreg  41486