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

Theorem simpr2r 1233
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 1189 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  poxp2  8128  poxp3  8135  frrlem8  8277  ttrcltr  9710  ttrclss  9714  rnttrcl  9716  ttrclselem2  9720  oppccatid  17664  subccatid  17795  setccatid  18033  catccatid  18055  estrccatid  18082  xpccatid  18139  gsmsymgreqlem1  19297  kerf1ghm  20281  ax5seg  28193  3pthdlem1  29414  segconeq  34977  ifscgr  35011  brofs2  35044  brifs2  35045  idinside  35051  btwnconn1lem8  35061  btwnconn1lem11  35064  btwnconn1lem12  35065  segcon2  35072  seglecgr12im  35077  unbdqndv2  35382  lplnexllnN  38430  paddasslem9  38694  paddasslem15  38700  pmodlem2  38713  lhp2lt  38867  isthincd2  47648  mndtccatid  47703
  Copyright terms: Public domain W3C validator