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  8148  poxp3  8155  frrlem8  8299  ttrcltr  9695  ttrclss  9699  rnttrcl  9701  ttrclselem2  9705  oppccatid  17800  subccatid  17928  setccatid  18166  catccatid  18188  estrccatid  18213  xpccatid  18269  kerf1ghm  19348  gsmsymgreqlem1  19531  ax5seg  29325  3pthdlem1  30552  segconeq  36523  ifscgr  36557  brofs2  36590  brifs2  36591  idinside  36597  btwnconn1lem8  36607  btwnconn1lem11  36610  btwnconn1lem12  36611  segcon2  36618  seglecgr12im  36623  unbdqndv2  37141  lplnexllnN  40379  paddasslem9  40643  paddasslem15  40649  pmodlem2  40662  lhp2lt  40816  ssccatid  49891  isthincd2  50256  mndtccatid  50406