Theorem simpr2r 1230

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  poxp2  8146  poxp3  8153  frrlem8  8297  ttrcltr  9749  ttrclss  9753  rnttrcl  9755  ttrclselem2  9759  oppccatid  17726  subccatid  17857  setccatid  18098  catccatid  18120  estrccatid  18147  xpccatid  18204  kerf1ghm  19234  gsmsymgreqlem1  19421  ax5seg  28866  3pthdlem1  30091  segconeq  35844  ifscgr  35878  brofs2  35911  brifs2  35912  idinside  35918  btwnconn1lem8  35928  btwnconn1lem11  35931  btwnconn1lem12  35932  segcon2  35939  seglecgr12im  35944  unbdqndv2  36224  lplnexllnN  39273  paddasslem9  39537  paddasslem15  39543  pmodlem2  39556  lhp2lt  39710  isthincd2  48392  mndtccatid  48447