![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.27 | Structured version Visualization 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 32 |
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 53 com23 81 pm3.2im 149 mth8 150 biimt 337 pm3.35 591 a2andOLD 821 pm2.26 894 cases2 983 19.35 1740 axc112 2020 issref 5213 tfinds 6686 tfindsg 6687 smogt 7086 findcard2 7811 findcard3 7814 fisupg 7819 xpfi 7842 dffi2 7937 fiinfg 8015 cantnfle 8176 ac5num 8467 pwsdompw 8634 cfsmolem 8700 axcc4 8869 axdc3lem2 8881 fpwwe2lem8 9062 pwfseqlem3 9085 tskord 9205 grudomon 9242 grur1a 9244 xrub 11597 relexprelg 13101 coprmproddvdslem 14679 pcmptcl 14836 restntr 20198 cmpsublem 20414 cmpsub 20415 txlm 20663 ptcmplem3 21069 c1lip1 22949 wilthlem3 23995 dmdbr5 27961 wzel 30507 waj-ax 31074 lukshef-ax2 31075 bj-axd2d 31176 bj-sbex 31239 bj-ssbeq 31240 bj-ssb0 31241 finixpnum 31930 mbfresfi 31987 filbcmb 32067 orfa 32315 axc11n-16 32509 axc11-o 32522 axc5c4c711toc7 36755 axc5c4c711to11 36756 ax6e2nd 36925 elex22VD 37235 exbiriVD 37250 ssralv2VD 37263 truniALTVD 37275 trintALTVD 37277 onfrALTVD 37288 hbimpgVD 37301 ax6e2eqVD 37304 ax6e2ndVD 37305 bgoldbwt 38878 bgoldbst 38879 nnsum4primesodd 38891 nnsum4primesoddALTV 38892 bgoldbnnsum3prm 38899 tgoldbach 38911 snlindsntor 40317 |
Copyright terms: Public domain | W3C validator |