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  1996  2mo  2053  euind  2656  reuind  2667  reuss2  3079  opelopabt  3818  reusv3i  4092  tfrlem5  5822  wemaplem2  6676  rlimcn2  10424  o1of2  10431  o1rlimmul  10436  2sqlem6  16103  spanuni  17463  pm11.71  22270
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