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

Theorem pm2.24 79
Description: Theorem *2.24 of [WhiteheadRussell] p. 104.
Assertion
Ref Expression
pm2.24 |- (ph -> (-. ph -> ps))

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 76 . 2 |- (-. ph -> (ph -> ps))
21com12 11 1 |- (ph -> (-. ph -> ps))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3
This theorem is referenced by:  pm4.81 163  oridm 243  orc 269  pm5.63 346  pm2.8 578  pm2.82 580  dedlema 764  prlem1 772  axpowndlem1 4961  ltlent 5534  ioojoint 6417
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
Copyright terms: Public domain