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  8124  poxp3  8131  frrlem8  8274  ttrcltr  9675  ttrclss  9679  rnttrcl  9681  ttrclselem2  9685  oppccatid  17686  subccatid  17814  setccatid  18052  catccatid  18074  estrccatid  18099  xpccatid  18155  kerf1ghm  19185  gsmsymgreqlem1  19366  ax5seg  28871  3pthdlem1  30099  segconeq  35993  ifscgr  36027  brofs2  36060  brifs2  36061  idinside  36067  btwnconn1lem8  36077  btwnconn1lem11  36080  btwnconn1lem12  36081  segcon2  36088  seglecgr12im  36093  unbdqndv2  36494  lplnexllnN  39553  paddasslem9  39817  paddasslem15  39823  pmodlem2  39836  lhp2lt  39990  ssccatid  49051  isthincd2  49416  mndtccatid  49566