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  2324  euind  3286  reuind  3303  reuss2  3777  reusv3i  4659  opelopabt  4764  wemaplem2  7993  rexanre  13179  rlimcn2  13413  o1of2  13435  o1rlimmul  13441  2sqlem6  23644  spanuni  26462  heicant  30049  pm11.71  31303
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