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  8083  poxp3  8090  frrlem8  8233  ttrcltr  9631  ttrclss  9635  rnttrcl  9637  ttrclselem2  9641  oppccatid  17643  subccatid  17771  setccatid  18009  catccatid  18031  estrccatid  18056  xpccatid  18112  kerf1ghm  19144  gsmsymgreqlem1  19327  ax5seg  28901  3pthdlem1  30126  segconeq  35983  ifscgr  36017  brofs2  36050  brifs2  36051  idinside  36057  btwnconn1lem8  36067  btwnconn1lem11  36070  btwnconn1lem12  36071  segcon2  36078  seglecgr12im  36083  unbdqndv2  36484  lplnexllnN  39543  paddasslem9  39807  paddasslem15  39813  pmodlem2  39826  lhp2lt  39980  ssccatid  49058  isthincd2  49423  mndtccatid  49573