HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem prth 554
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 283 . . . . 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 365 1 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  anim12d 556  mo 1370  2mo 1424  reuss2 2246  ssxp 3218  tfrlem5 3854  cau3ir 6803  cvganz 6812  clm3 6968  climunii 6986  climaddlem3 7003  climmullem8 7014  xplm 7857  xpcn 7858  lmcau 7878  hlimcaui 9257  hlimunii 9259  spanun 9596
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 147  df-an 225
Copyright terms: Public domain