Theorem simpr2r 1231

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 1187	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1085

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 400  df-3an 1087

This theorem is referenced by:  oppccatid  17062  subccatid  17190  setccatid  17425  catccatid  17443  estrccatid  17463  xpccatid  17519  gsmsymgreqlem1  18640  kerf1ghm  19581  ax5seg  26846  3pthdlem1  28063  poxp2  33359  frrlem8  33406  segconeq  33897  ifscgr  33931  brofs2  33964  brifs2  33965  idinside  33971  btwnconn1lem8  33981  btwnconn1lem11  33984  btwnconn1lem12  33985  segcon2  33992  seglecgr12im  33997  unbdqndv2  34276  lplnexllnN  37176  paddasslem9  37440  paddasslem15  37446  pmodlem2  37459  lhp2lt  37613