![]() |
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 240 pm3.35 345 pm3.2im 627 jcn 641 pm2.65 649 annimim 676 condcOLD 840 pm2.26dc 893 ax10o 1694 issref 4929 acexmidlem2 5779 findcard2 6791 findcard2s 6792 xpfi 6826 txlm 12487 bj-inf2vnlem1 13339 bj-findis 13348 |
Copyright terms: Public domain | W3C validator |