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

Theorem prth 558
Description: Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema.'
Assertion
Ref Expression
prth |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))

Proof of Theorem prth
StepHypRef Expression
1 pm3.2 281 . . . . 5 |- (ps -> (th -> (ps /\ th)))
21imim2d 25 . . . 4 |- (ps -> ((ch -> th) -> (ch -> (ps /\ th))))
32imim2i 17 . . 3 |- ((ph -> ps) -> (ph -> ((ch -> th) -> (ch -> (ps /\ th)))))
43com23 32 . 2 |- ((ph -> ps) -> ((ch -> th) -> (ph -> (ch -> (ps /\ th)))))
54imp4b 363 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 221
This theorem is referenced by:  anim12d 560  mo 1430  2mo 1485  reuss2 2325  ssxp 3342  tfrlem5 4211  cau3iri 7106  cvganz 7115  clm3i 7270  climunii 7289  climaddlem3 7307  climmullem8 7318  xplm 8173  xpcn 8174  lmcau 8194  hlimcauii 9359  hlimuniii 9361  spanuni 9720
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 145  df-an 223
Copyright terms: Public domain