Theorem simpr2r 1240

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  poxp3  8097  frrlem8  8240  ttrcltr  9635  ttrclss  9639  rnttrcl  9641  ttrclselem2  9645  oppccatid  17683  subccatid  17811  setccatid  18049  catccatid  18071  estrccatid  18096  xpccatid  18152  kerf1ghm  19220  gsmsymgreqlem1  19403  ax5seg  29032  3pthdlem1  30259  segconeq  36245  ifscgr  36279  brofs2  36312  brifs2  36313  idinside  36319  btwnconn1lem8  36329  btwnconn1lem11  36332  btwnconn1lem12  36333  segcon2  36340  seglecgr12im  36345  unbdqndv2  36824  lplnexllnN  40063  paddasslem9  40327  paddasslem15  40333  pmodlem2  40346  lhp2lt  40500  ssccatid  49569  isthincd2  49934  mndtccatid  50084