Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.27 | Unicode version |
Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 5. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
pm2.27 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | 1 | com12 30 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: pm2.43 53 com23 78 biimt 240 pm3.35 345 pm3.2im 632 jcn 646 pm2.65 654 annimim 681 condcOLD 849 pm2.26dc 902 ax10o 1708 issref 4993 acexmidlem2 5850 findcard2 6867 findcard2s 6868 xpfi 6907 exmidontriim 7202 pcmptcl 12294 txlm 13073 bj-inf2vnlem1 14005 bj-findis 14014 |
Copyright terms: Public domain | W3C validator |