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

Theorem simpr1r 1307
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 789 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜓)
213ad2antr1 1239 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  oppccatid  16647  subccatid  16774  setccatid  17002  catccatid  17020  estrccatid  17040  xpccatid  17097  gsmsymgreqlem1  18116  dmdprdsplit  18716  neitr  21267  neitx  21693  tx1stc  21736  utop3cls  22337  metustsym  22642  clwwlkccat  27220  3pthdlem1  27445  archiabllem1  30197  esumpcvgval  30590  esum2d  30605  ifscgr  32598  btwnconn1lem8  32648  btwnconn1lem11  32651  btwnconn1lem12  32652  segletr  32668  broutsideof3  32680  unbdqndv2  32944  lhp2lt  35960  cdlemf2  36521  cdlemn11pre  37169  stoweidlem60  40917
  Copyright terms: Public domain W3C validator