HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem prth 548
Description: Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema' (splendid theorem). (The proof was shortened by Wolf Lammen, 7-Apr-2013.)
Assertion
Ref Expression
prth

Proof of Theorem prth
StepHypRef Expression
1 simpl 436 . 2
2 simpr 440 . 2
31, 2anim12d 541 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357
This theorem is referenced by:  mo 1830  2mo 1887  euind 2483  reuind 2494  reuss2 2901  opelopabt 3621  reusv3i 3879  tfrlem5 5518  wemaplem2 6245  rlimcn2 9603  o1of2 9610  o1rlimmul 9615  spanuni 15629  pm11.71 21434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 175  df-an 359
Copyright terms: Public domain