![]() |
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: ![]() |
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 241 pm3.35 347 pm3.2im 637 jcn 651 pm2.65 659 annimim 686 condcOLD 854 pm2.26dc 907 ax10o 1715 issref 5011 acexmidlem2 5871 findcard2 6888 findcard2s 6889 xpfi 6928 exmidontriim 7223 pcmptcl 12334 txlm 13672 bj-inf2vnlem1 14604 bj-findis 14613 |
Copyright terms: Public domain | W3C validator |