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

Theorem prth 547
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 435 . 2
2 simpr 439 . 2
31, 2anim12d 540 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 356
This theorem is referenced by:  mo 1829  2mo 1886  euind 2478  reuind 2489  reuss2 2892  opelopabt 3583  reusv3i 3840  tfrlem5 5407  rlimcn2 9314  o1of2 9321  o1rlimmul 9326  spanuni 14220  wemapso2 18877  pm11.71 19415
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 174  df-an 358
Copyright terms: Public domain