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

Theorem simpr1r 1292
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 750 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1203 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  oppccatid  16587  subccatid  16714  setccatid  16942  catccatid  16960  estrccatid  16980  xpccatid  17037  gsmsymgreqlem1  18058  dmdprdsplit  18655  neitr  21206  neitx  21632  tx1stc  21675  utop3cls  22276  metustsym  22581  clwwlkccat  27141  3pthdlem1  27345  archiabllem1  30088  esumpcvgval  30481  esum2d  30496  ifscgr  32489  btwnconn1lem8  32539  btwnconn1lem11  32542  btwnconn1lem12  32543  segletr  32559  broutsideof3  32571  unbdqndv2  32840  lhp2lt  35810  cdlemf2  36372  cdlemn11pre  37021  stoweidlem60  40795
  Copyright terms: Public domain W3C validator