![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > imp32 | Structured version Unicode version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp3.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imp32 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | impd 431 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 429 |
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 depends on definitions: df-bi 185 df-an 371 |
This theorem is referenced by: imp42 594 impr 619 anasss 647 an13s 801 3expb 1189 reuss2 3737 reupick 3741 po2nr 4761 tz7.7 4852 ordtr2 4870 fvmptt 5897 fliftfund 6114 isomin 6136 f1ocnv2d 6420 onint 6515 tz7.48lem 7005 oalimcl 7108 oaass 7109 omass 7128 omabs 7195 finsschain 7728 infxpenlem 8290 axcc3 8717 zorn2lem7 8781 addclpi 9171 addnidpi 9180 genpnnp 9284 genpnmax 9286 mulclprlem 9298 dedekindle 9644 prodgt0 10284 ltsubrp 11132 ltaddrp 11133 swrdccatin1 12491 swrdccat3 12500 infpnlem1 14088 iscatd 14729 imasmnd2 15576 imasgrp2 15788 imasrng 16833 mplcoe5lem 17670 0ntr 18806 clsndisj 18810 innei 18860 islpi 18884 tgcnp 18988 haust1 19087 alexsublem 19747 alexsubb 19749 isxmetd 20032 axcontlem4 23364 grpoidinvlem3 23844 elspansn5 25128 5oalem6 25213 mdi 25850 dmdi 25857 dmdsl3 25870 atom1d 25908 cvexchlem 25923 atcvatlem 25940 chirredlem3 25947 mdsymlem5 25962 f1o3d 26098 dfon2lem6 27744 frmin 27846 soseq 27858 nodenselem5 27969 nodense 27973 broutsideof2 28296 outsideoftr 28303 outsideofeq 28304 nndivsub 28446 bddiblnc 28609 ftc1anc 28622 elicc3 28659 nn0prpwlem 28664 cntotbnd 28842 heiborlem6 28862 pridlc3 29020 wwlknimp 30468 wlkiswwlksur 30498 clwwlkf 30603 clwwlkextfrlem1 30816 dmatmul 31041 scmatmulcl 31051 scmatsgrp1 31054 cpmatacl 31191 cpmatmcllem 31193 bnj570 32215 leat2 33262 cvrexchlem 33386 cvratlem 33388 3dim2 33435 ps-2 33445 lncvrelatN 33748 osumcllem11N 33933 |
Copyright terms: Public domain | W3C validator |