Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpr2r Structured version   Visualization version   GIF version

Theorem simpr2r 1231
 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
StepHypRef Expression
1 simprr 772 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr2 1187 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1085 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 210  df-an 400  df-3an 1087 This theorem is referenced by:  oppccatid  17062  subccatid  17190  setccatid  17425  catccatid  17443  estrccatid  17463  xpccatid  17519  gsmsymgreqlem1  18640  kerf1ghm  19581  ax5seg  26846  3pthdlem1  28063  poxp2  33359  frrlem8  33406  segconeq  33897  ifscgr  33931  brofs2  33964  brifs2  33965  idinside  33971  btwnconn1lem8  33981  btwnconn1lem11  33984  btwnconn1lem12  33985  segcon2  33992  seglecgr12im  33997  unbdqndv2  34276  lplnexllnN  37176  paddasslem9  37440  paddasslem15  37446  pmodlem2  37459  lhp2lt  37613
 Copyright terms: Public domain W3C validator