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  8085  poxp3  8092  frrlem8  8235  ttrcltr  9625  ttrclss  9629  rnttrcl  9631  ttrclselem2  9635  oppccatid  17642  subccatid  17770  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  kerf1ghm  19176  gsmsymgreqlem1  19359  ax5seg  29011  3pthdlem1  30239  segconeq  36204  ifscgr  36238  brofs2  36271  brifs2  36272  idinside  36278  btwnconn1lem8  36288  btwnconn1lem11  36291  btwnconn1lem12  36292  segcon2  36299  seglecgr12im  36304  unbdqndv2  36711  lplnexllnN  39820  paddasslem9  40084  paddasslem15  40090  pmodlem2  40103  lhp2lt  40257  ssccatid  49313  isthincd2  49678  mndtccatid  49828