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  8142  poxp3  8149  frrlem8  8292  ttrcltr  9730  ttrclss  9734  rnttrcl  9736  ttrclselem2  9740  oppccatid  17731  subccatid  17859  setccatid  18097  catccatid  18119  estrccatid  18144  xpccatid  18200  kerf1ghm  19230  gsmsymgreqlem1  19411  ax5seg  28917  3pthdlem1  30145  segconeq  36028  ifscgr  36062  brofs2  36095  brifs2  36096  idinside  36102  btwnconn1lem8  36112  btwnconn1lem11  36115  btwnconn1lem12  36116  segcon2  36123  seglecgr12im  36128  unbdqndv2  36529  lplnexllnN  39583  paddasslem9  39847  paddasslem15  39853  pmodlem2  39866  lhp2lt  40020  ssccatid  49039  isthincd2  49323  mndtccatid  49464