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 1431  2mo 1486  reuss2 2326  ssxp 3344  tfrlem5 4214  cau3iri 7116  cvganz 7125  clm3i 7280  climunii 7299  climaddlem3 7317  climmullem8 7328  xplm 8184  xpcn 8185  lmcau 8205  hlimcauii 9376  hlimuniii 9378  spanuni 9737  heiborlem36 11939
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