MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prth Unicode version

Theorem prth 571
Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 563. 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). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Assertion
Ref Expression
prth

Proof of Theorem prth
StepHypRef Expression
1 simpl 457 . 2
2 simpr 461 . 2
31, 2anim12d 563 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mo3OLD  2308  moOLD  2314  2moOLDOLD  2371  euind  3256  reuind  3273  reuss2  3744  reusv3i  4616  opelopabt  4718  wemaplem2  7898  rexanre  12992  rlimcn2  13226  o1of2  13248  o1rlimmul  13254  2sqlem6  23108  spanuni  25416  heicant  28886  pm11.71  30110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator