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  8135  poxp3  8142  frrlem8  8286  ttrcltr  9681  ttrclss  9685  rnttrcl  9687  ttrclselem2  9691  oppccatid  17771  subccatid  17899  setccatid  18137  catccatid  18159  estrccatid  18184  xpccatid  18240  kerf1ghm  19313  gsmsymgreqlem1  19496  ax5seg  29225  3pthdlem1  30452  segconeq  36397  ifscgr  36431  brofs2  36464  brifs2  36465  idinside  36471  btwnconn1lem8  36481  btwnconn1lem11  36484  btwnconn1lem12  36485  segcon2  36492  seglecgr12im  36497  unbdqndv2  36985  lplnexllnN  40223  paddasslem9  40487  paddasslem15  40493  pmodlem2  40506  lhp2lt  40660  ssccatid  49728  isthincd2  50093  mndtccatid  50243