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  8145  poxp3  8152  frrlem8  8296  ttrcltr  9699  ttrclss  9703  rnttrcl  9705  ttrclselem2  9709  oppccatid  17813  subccatid  17941  setccatid  18179  catccatid  18201  estrccatid  18226  xpccatid  18282  kerf1ghm  19380  gsmsymgreqlem1  19563  ax5seg  29403  3pthdlem1  30652  segconeq  36598  ifscgr  36632  brofs2  36665  brifs2  36666  idinside  36672  btwnconn1lem8  36682  btwnconn1lem11  36685  btwnconn1lem12  36686  segcon2  36693  seglecgr12im  36698  unbdqndv2  37216  lplnexllnN  40445  paddasslem9  40709  paddasslem15  40715  pmodlem2  40728  lhp2lt  40882  ssccatid  50006  isthincd2  50371  mndtccatid  50521