![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.24 | Structured version Visualization version Unicode version |
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 138. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 112 |
. 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 ax-3 8 |
This theorem is referenced by: pm4.81 372 orc 391 pm2.82 868 dedlema 971 cases2 989 eqneqall 2645 suppimacnv 6951 ressuppss 6960 ressuppssdif 6962 infssuni 7890 axpowndlem1 9047 ltlen 9760 znnn0nn 11075 elfzonlteqm1 12019 injresinjlem 12055 ssnn0fi 12228 hasheqf1oi 12565 swrdnd2 12825 swrdccat3blem 12887 repswswrd 12923 mdegle0 23074 nb3graprlem1 25227 nbcusgra 25239 wlkdvspthlem 25385 clwwlkprop 25546 hashnbgravdg 25689 4cyclusnfrgra 25795 broutsideof2 30937 meran1 31119 bj-andnotim 31216 contrd 32377 pell1qrgaplem 35763 pm2.43cbi 36918 zeo2ALTV 38837 elnelall 39019 nb3grprlem1 39503 ztprmneprm 40400 |
Copyright terms: Public domain | W3C validator |