Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.27 | GIF 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 344 pm3.2im 611 mth8 624 pm2.65 633 annimim 660 condcOLD 824 pm2.26dc 877 ax10o 1678 issref 4891 acexmidlem2 5739 findcard2 6751 findcard2s 6752 xpfi 6786 txlm 12375 bj-inf2vnlem1 13095 bj-findis 13104 |
Copyright terms: Public domain | W3C validator |