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  8093  poxp3  8100  frrlem8  8243  ttrcltr  9637  ttrclss  9641  rnttrcl  9643  ttrclselem2  9647  oppccatid  17685  subccatid  17813  setccatid  18051  catccatid  18073  estrccatid  18098  xpccatid  18154  kerf1ghm  19222  gsmsymgreqlem1  19405  ax5seg  29007  3pthdlem1  30234  segconeq  36192  ifscgr  36226  brofs2  36259  brifs2  36260  idinside  36266  btwnconn1lem8  36276  btwnconn1lem11  36279  btwnconn1lem12  36280  segcon2  36287  seglecgr12im  36292  unbdqndv2  36771  lplnexllnN  40010  paddasslem9  40274  paddasslem15  40280  pmodlem2  40293  lhp2lt  40447  ssccatid  49547  isthincd2  49912  mndtccatid  50062