![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pm2.27 | Structured version 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, 15-Jul-1993.) |
Ref | Expression |
---|---|
pm2.27 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 31 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar 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 51 com23 78 pm3.2im 145 mth8 146 biimt 335 pm3.35 587 pm2.26 878 cases2 963 19.35 1655 axc112 1872 axc11n-16 2246 axc11-o 2259 issref 5311 tfinds 6572 tfindsg 6573 smogt 6930 findcard2 7655 findcard3 7658 fisupg 7663 xpfi 7686 dffi2 7776 cantnfle 7982 cantnfleOLD 8012 ac5num 8309 pwsdompw 8476 cfsmolem 8542 axcc4 8711 axdc3lem2 8723 fpwwe2lem8 8907 pwfseqlem3 8930 tskord 9050 grudomon 9087 grur1a 9089 xrub 11377 pcmptcl 14057 restntr 18904 cmpsublem 19120 cmpsub 19121 bwthOLD 19132 txlm 19339 ptcmplem3 19744 c1lip1 21587 wilthlem3 22526 dmdbr5 25849 wzel 27897 waj-ax 28396 lukshef-ax2 28397 finixpnum 28554 mbfresfi 28578 filbcmb 28774 orfa 29022 axc5c4c711toc7 29798 axc5c4c711to11 29799 a2and 30856 snlindsntor 31114 ax6e2nd 31569 elex22VD 31877 exbiriVD 31892 ssralv2VD 31904 truniALTVD 31916 trintALTVD 31918 onfrALTVD 31929 hbimpgVD 31942 ax6e2eqVD 31945 ax6e2ndVD 31946 bj-axd2d 32430 |
Copyright terms: Public domain | W3C validator |