Theorem simpr2r 1235

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp2  8095  poxp3  8102  frrlem8  8245  ttrcltr  9637  ttrclss  9641  rnttrcl  9643  ttrclselem2  9647  oppccatid  17654  subccatid  17782  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  kerf1ghm  19188  gsmsymgreqlem1  19371  ax5seg  29023  3pthdlem1  30251  segconeq  36223  ifscgr  36257  brofs2  36290  brifs2  36291  idinside  36297  btwnconn1lem8  36307  btwnconn1lem11  36310  btwnconn1lem12  36311  segcon2  36318  seglecgr12im  36323  unbdqndv2  36730  lplnexllnN  39934  paddasslem9  40198  paddasslem15  40204  pmodlem2  40217  lhp2lt  40371  ssccatid  49425  isthincd2  49790  mndtccatid  49940