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

Theorem potr 5602
Description: A partial order is a transitive relation. (Contributed by NM, 27-Mar-1997.)
Assertion
Ref Expression
potr ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))

Proof of Theorem potr
StepHypRef Expression
1 pocl 5596 . . 3 (𝑅 Po 𝐴 → ((𝐵𝐴𝐶𝐴𝐷𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
21imp 408 . 2 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷)))
32simprd 497 1 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088  wcel 2107   class class class wbr 5149   Po wpo 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-po 5589
This theorem is referenced by:  po2nr  5603  po3nr  5604  pofun  5607  sotr  5613  poltletr  6134  frpomin  6342  poxp  8114  poxp2  8129  poxp3  8136  poseq  8144  fprlem2  8286  frfi  9288  wemaplem2  9542  sornom  10272  zorn2lem7  10497  pospo  18298  pocnv  34733  seqpo  36615  oneptr  42004
  Copyright terms: Public domain W3C validator