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

Theorem prth 552
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 440 . 2
2 simpr 444 . 2
31, 2anim12d 545 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 360
This theorem is referenced by:  mo 1841  2mo 1898  euind 2489  reuind 2500  reuss2 2893  opelopabt 3583  reusv3i 3838  tfrlem5 5346  rlimcn2 9201  o1of2 9208  o1rlimmul 9213  spanuni 13610  pm11.71 18338
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 362
Copyright terms: Public domain