Theorem simpr2r 1232

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 770	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2antr2 1188	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  frrlem8  8109  ttrcltr  9474  ttrclss  9478  rnttrcl  9480  ttrclselem2  9484  oppccatid  17430  subccatid  17561  setccatid  17799  catccatid  17821  estrccatid  17848  xpccatid  17905  gsmsymgreqlem1  19038  kerf1ghm  19987  ax5seg  27306  3pthdlem1  28528  poxp2  33790  segconeq  34312  ifscgr  34346  brofs2  34379  brifs2  34380  idinside  34386  btwnconn1lem8  34396  btwnconn1lem11  34399  btwnconn1lem12  34400  segcon2  34407  seglecgr12im  34412  unbdqndv2  34691  lplnexllnN  37578  paddasslem9  37842  paddasslem15  37848  pmodlem2  37861  lhp2lt  38015  isthincd2  46319  mndtccatid  46374