Theorem simpr2r 1252

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8162  poxp3  8169  frrlem8  8314  ttrcltr  9720  ttrclss  9724  rnttrcl  9726  ttrclselem2  9730  oppccatid  17898  subccatid  18026  setccatid  18264  catccatid  18286  estrccatid  18311  xpccatid  18367  kerf1ghm  19466  gsmsymgreqlem1  19649  ax5seg  29521  3pthdlem1  30770  segconeq  36867  ifscgr  36901  brofs2  36934  brifs2  36935  idinside  36941  btwnconn1lem8  36951  btwnconn1lem11  36954  btwnconn1lem12  36955  segcon2  36962  seglecgr12im  36967  unbdqndv2  37469  lplnexllnN  40714  paddasslem9  40978  paddasslem15  40984  pmodlem2  40997  lhp2lt  41151  ssccatid  50279  isthincd2  50665  mndtccatid  50818