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 2482  reuind 2493  reuss2 2898  opelopabt 3609  reusv3i 3866  tfrlem5 5481  wemaplem2 6212  rlimcn2 9455  o1of2 9462  o1rlimmul 9467  spanuni 15112  pm11.71 20736
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