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  8125  poxp3  8132  frrlem8  8275  ttrcltr  9676  ttrclss  9680  rnttrcl  9682  ttrclselem2  9686  oppccatid  17687  subccatid  17815  setccatid  18053  catccatid  18075  estrccatid  18100  xpccatid  18156  kerf1ghm  19186  gsmsymgreqlem1  19367  ax5seg  28872  3pthdlem1  30100  segconeq  36005  ifscgr  36039  brofs2  36072  brifs2  36073  idinside  36079  btwnconn1lem8  36089  btwnconn1lem11  36092  btwnconn1lem12  36093  segcon2  36100  seglecgr12im  36105  unbdqndv2  36506  lplnexllnN  39565  paddasslem9  39829  paddasslem15  39835  pmodlem2  39848  lhp2lt  40002  ssccatid  49065  isthincd2  49430  mndtccatid  49580