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

Theorem simpr1r 1232
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpr1r ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)

Proof of Theorem simpr1r
StepHypRef Expression
1 simprr 772 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1189 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  poxp2  8124  oppccatid  17661  subccatid  17792  setccatid  18030  catccatid  18052  estrccatid  18079  xpccatid  18136  gsmsymgreqlem1  19291  dmdprdsplit  19909  neitr  22666  neitx  23093  tx1stc  23136  utop3cls  23738  metustsym  24046  clwwlkccat  29223  3pthdlem1  29397  archiabllem1  32317  esumpcvgval  33014  esum2d  33029  ifscgr  34954  btwnconn1lem8  35004  btwnconn1lem11  35007  btwnconn1lem12  35008  segletr  35024  broutsideof3  35036  unbdqndv2  35325  lhp2lt  38810  cdlemf2  39371  cdlemn11pre  40019  stoweidlem60  44711  isthincd2  47560  mndtccatid  47615
  Copyright terms: Public domain W3C validator