Theorem simpr2r 1296

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  oppccatid  16586  subccatid  16713  setccatid  16941  catccatid  16959  estrccatid  16979  xpccatid  17036  gsmsymgreqlem1  18057  kerf1hrm  18953  ax5seg  26039  3pthdlem1  27344  frrlem11  32129  segconeq  32454  ifscgr  32488  brofs2  32521  brifs2  32522  idinside  32528  btwnconn1lem8  32538  btwnconn1lem11  32541  btwnconn1lem12  32542  segcon2  32549  seglecgr12im  32554  unbdqndv2  32839  lplnexllnN  35372  paddasslem9  35636  paddasslem15  35642  pmodlem2  35655  lhp2lt  35809