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 1942  2mo 1999  euind 2596  reuind 2607  reuss2 3019  opelopabt 3757  reusv3i 4016  tfrlem5 5730  wemaplem2 6530  rlimcn2 10261  o1of2 10268  o1rlimmul 10273  2sqlem6 15797  spanuni 17175  pm11.71 21972
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