Theorem simpr2r 1234

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpr2r

Step	Hyp	Ref	Expression
1		simprr 772	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2antr2 1190	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

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

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 1088

This theorem is referenced by:  poxp2  8079  poxp3  8086  frrlem8  8229  ttrcltr  9613  ttrclss  9617  rnttrcl  9619  ttrclselem2  9623  oppccatid  17627  subccatid  17755  setccatid  17993  catccatid  18015  estrccatid  18040  xpccatid  18096  kerf1ghm  19161  gsmsymgreqlem1  19344  ax5seg  28918  3pthdlem1  30146  segconeq  36075  ifscgr  36109  brofs2  36142  brifs2  36143  idinside  36149  btwnconn1lem8  36159  btwnconn1lem11  36162  btwnconn1lem12  36163  segcon2  36170  seglecgr12im  36175  unbdqndv2  36576  lplnexllnN  39683  paddasslem9  39947  paddasslem15  39953  pmodlem2  39966  lhp2lt  40120  ssccatid  49197  isthincd2  49562  mndtccatid  49712