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  8086  poxp3  8093  frrlem8  8236  ttrcltr  9628  ttrclss  9632  rnttrcl  9634  ttrclselem2  9638  oppccatid  17676  subccatid  17804  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  kerf1ghm  19213  gsmsymgreqlem1  19396  ax5seg  29021  3pthdlem1  30249  segconeq  36208  ifscgr  36242  brofs2  36275  brifs2  36276  idinside  36282  btwnconn1lem8  36292  btwnconn1lem11  36295  btwnconn1lem12  36296  segcon2  36303  seglecgr12im  36308  unbdqndv2  36787  lplnexllnN  40024  paddasslem9  40288  paddasslem15  40294  pmodlem2  40307  lhp2lt  40461  ssccatid  49559  isthincd2  49924  mndtccatid  50074