Theorem simpr2r 1229

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oppccatid  16991  subccatid  17118  setccatid  17346  catccatid  17364  estrccatid  17384  xpccatid  17440  gsmsymgreqlem1  18560  kerf1ghm  19499  kerf1hrmOLD  19500  ax5seg  26726  3pthdlem1  27945  frrlem8  33132  segconeq  33473  ifscgr  33507  brofs2  33540  brifs2  33541  idinside  33547  btwnconn1lem8  33557  btwnconn1lem11  33560  btwnconn1lem12  33561  segcon2  33568  seglecgr12im  33573  unbdqndv2  33852  lplnexllnN  36702  paddasslem9  36966  paddasslem15  36972  pmodlem2  36985  lhp2lt  37139