Theorem simpr2r 1252

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8144  poxp3  8151  frrlem8  8295  ttrcltr  9701  ttrclss  9705  rnttrcl  9707  ttrclselem2  9711  oppccatid  17873  subccatid  18001  setccatid  18239  catccatid  18261  estrccatid  18286  xpccatid  18342  kerf1ghm  19441  gsmsymgreqlem1  19624  ax5seg  29498  3pthdlem1  30747  segconeq  36745  ifscgr  36779  brofs2  36812  brifs2  36813  idinside  36819  btwnconn1lem8  36829  btwnconn1lem11  36832  btwnconn1lem12  36833  segcon2  36840  seglecgr12im  36845  unbdqndv2  37347  lplnexllnN  40589  paddasslem9  40853  paddasslem15  40859  pmodlem2  40872  lhp2lt  41026  ssccatid  50124  isthincd2  50489  mndtccatid  50639