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  8187  poxp3  8194  frrlem8  8339  ttrcltr  9744  ttrclss  9748  rnttrcl  9750  ttrclselem2  9754  oppccatid  17922  subccatid  18050  setccatid  18288  catccatid  18310  estrccatid  18335  xpccatid  18391  kerf1ghm  19490  gsmsymgreqlem1  19674  ax5seg  29546  3pthdlem1  30795  segconeq  36953  ifscgr  36987  brofs2  37020  brifs2  37021  idinside  37027  btwnconn1lem8  37037  btwnconn1lem11  37040  btwnconn1lem12  37041  segcon2  37048  seglecgr12im  37053  unbdqndv2  37555  lplnexllnN  40813  paddasslem9  41077  paddasslem15  41083  pmodlem2  41096  lhp2lt  41250  ssccatid  50391  isthincd2  50777  mndtccatid  50930