Theorem simpr2r 1250

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp2  8127  poxp3  8134  frrlem8  8278  ttrcltr  9673  ttrclss  9677  rnttrcl  9679  ttrclselem2  9683  oppccatid  17765  subccatid  17893  setccatid  18131  catccatid  18153  estrccatid  18178  xpccatid  18234  kerf1ghm  19308  gsmsymgreqlem1  19491  ax5seg  29197  3pthdlem1  30424  segconeq  36373  ifscgr  36407  brofs2  36440  brifs2  36441  idinside  36447  btwnconn1lem8  36457  btwnconn1lem11  36460  btwnconn1lem12  36461  segcon2  36468  seglecgr12im  36473  unbdqndv2  36962  lplnexllnN  40200  paddasslem9  40464  paddasslem15  40470  pmodlem2  40483  lhp2lt  40637  ssccatid  49701  isthincd2  50066  mndtccatid  50216