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

Theorem simpr2r 1230
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 771 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr2 1186 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  poxp2  8146  poxp3  8153  frrlem8  8297  ttrcltr  9749  ttrclss  9753  rnttrcl  9755  ttrclselem2  9759  oppccatid  17726  subccatid  17857  setccatid  18098  catccatid  18120  estrccatid  18147  xpccatid  18204  kerf1ghm  19234  gsmsymgreqlem1  19421  ax5seg  28866  3pthdlem1  30091  segconeq  35844  ifscgr  35878  brofs2  35911  brifs2  35912  idinside  35918  btwnconn1lem8  35928  btwnconn1lem11  35931  btwnconn1lem12  35932  segcon2  35939  seglecgr12im  35944  unbdqndv2  36224  lplnexllnN  39273  paddasslem9  39537  paddasslem15  39543  pmodlem2  39556  lhp2lt  39710  isthincd2  48392  mndtccatid  48447
  Copyright terms: Public domain W3C validator