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

Theorem simpr1r 1225
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 769 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1182 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  oppccatid  16982  subccatid  17109  setccatid  17337  catccatid  17355  estrccatid  17375  xpccatid  17431  gsmsymgreqlem1  18481  dmdprdsplit  19092  neitr  21707  neitx  22134  tx1stc  22177  utop3cls  22778  metustsym  23083  clwwlkccat  27685  3pthdlem1  27860  archiabllem1  30739  esumpcvgval  31226  esum2d  31241  ifscgr  33392  btwnconn1lem8  33442  btwnconn1lem11  33445  btwnconn1lem12  33446  segletr  33462  broutsideof3  33474  unbdqndv2  33737  lhp2lt  37007  cdlemf2  37568  cdlemn11pre  38216  stoweidlem60  42214
  Copyright terms: Public domain W3C validator