Theorem simpr2r 1234

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8073  poxp3  8080  frrlem8  8223  ttrcltr  9606  ttrclss  9610  rnttrcl  9612  ttrclselem2  9616  oppccatid  17622  subccatid  17750  setccatid  17988  catccatid  18010  estrccatid  18035  xpccatid  18091  kerf1ghm  19157  gsmsymgreqlem1  19340  ax5seg  28914  3pthdlem1  30139  segconeq  36043  ifscgr  36077  brofs2  36110  brifs2  36111  idinside  36117  btwnconn1lem8  36127  btwnconn1lem11  36130  btwnconn1lem12  36131  segcon2  36138  seglecgr12im  36143  unbdqndv2  36544  lplnexllnN  39602  paddasslem9  39866  paddasslem15  39872  pmodlem2  39885  lhp2lt  40039  ssccatid  49103  isthincd2  49468  mndtccatid  49618