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

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

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 1089

This theorem is referenced by:  poxp2  8168  poxp3  8175  frrlem8  8318  ttrcltr  9756  ttrclss  9760  rnttrcl  9762  ttrclselem2  9766  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  kerf1ghm  19265  gsmsymgreqlem1  19448  ax5seg  28953  3pthdlem1  30183  segconeq  36011  ifscgr  36045  brofs2  36078  brifs2  36079  idinside  36085  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  segcon2  36106  seglecgr12im  36111  unbdqndv2  36512  lplnexllnN  39566  paddasslem9  39830  paddasslem15  39836  pmodlem2  39849  lhp2lt  40003  isthincd2  49086  mndtccatid  49184