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

Theorem prth 796
 Description: Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 599. 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 475 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → (𝜑𝜓))
2 simpr 477 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → (𝜒𝜃))
31, 2anim12d 599 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → ((𝜑𝜒) → (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 387 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 199  df-an 388 This theorem is referenced by:  euind  3627  reuind  3653  reusv3i  5158  opelopabt  5273  wemaplem2  8806  rexanre  14567  rlimcn2  14808  o1of2  14830  o1rlimmul  14836  2sqlem6  25701  spanuni  29102  isbasisrelowllem1  34084  isbasisrelowllem2  34085  heicant  34374  pm11.71  40152
 Copyright terms: Public domain W3C validator