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

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

Proof of Theorem potr
StepHypRef Expression
1 pocl 5479 . . 3 (𝑅 Po 𝐴 → ((𝐵𝐴𝐶𝐴𝐷𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
21imp 407 . 2 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷)))
32simprd 496 1 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1081  wcel 2107   class class class wbr 5062   Po wpo 5470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-po 5472
This theorem is referenced by:  po2nr  5485  po3nr  5486  pofun  5489  sotr  5495  poltletr  5989  predpo  6163  poxp  7816  frfi  8755  wemaplem2  9003  sornom  9691  zorn2lem7  9916  pospo  17575  pocnv  32885  frpomin  32964  poseq  32981  fprlem2  33024  seqpo  34892
  Copyright terms: Public domain W3C validator