![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con4i | Structured version Visualization version Unicode version |
Description: Inference associated with con4 107. Its associated inference is mt4 144. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 21-Jun-2013.) |
Ref | Expression |
---|---|
con4i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con4i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot1 126 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | con4i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | nsyl2 132 |
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: pm2.21i 136 mt4 144 modal-b 1961 elimasni 5201 ndmfvrcl 5904 brabv 6354 oprssdm 6469 ndmovrcl 6474 omelon2 6723 omopthi 7376 fsuppres 7926 sdomsdomcardi 8423 alephgeom 8531 pwcdadom 8664 rankcf 9220 adderpq 9399 mulerpq 9400 ssnn0fi 12235 sadcp1 14508 setcepi 16061 oduclatb 16468 cntzrcl 17059 pmtrfrn 17177 dprddomcld 17711 dprdsubg 17735 psrbagsn 18795 dsmmbas2 19377 dsmmfi 19378 istps 20028 isusp 21354 dscmet 21665 dscopn 21666 i1f1lem 22726 sqff1o 24188 umgrafi 25128 usgraedgrnv 25183 nbgranself2 25243 wwlknndef 25544 clwwlknndef 25580 dmadjrnb 27640 axpowprim 30403 opelco3 30491 sltintdifex 30621 bj-modal5e 31313 bj-modal4e 31374 topdifinffinlem 31820 finxp1o 31854 ax6fromc10 32532 axc711to11 32552 axc5c711to11 32556 pw2f1ocnv 35963 kelac1 35992 relintabex 36258 axc5c4c711toc5 36823 axc5c4c711to11 36826 disjrnmpt2 37534 afvvdm 38788 afvvfunressn 38790 afvvv 38792 afvfv0bi 38799 upgrfi 39337 |
Copyright terms: Public domain | W3C validator |