![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con3dimp | Structured version Visualization version Unicode version |
Description: Variant of con3d 140 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
con3dimp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con3dimp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3dimp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con3d 140 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 435 |
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 190 df-an 377 |
This theorem is referenced by: nelneq 2564 nelneq2 2565 nelss 3503 dtru 4611 sofld 5306 card2inf 8101 gchen1 9081 gchen2 9082 bcpasc 12544 fiinfnf1o 12571 hashfn 12592 swrdnd2 12832 swrdccat 12892 pcprod 14895 lubval 16285 glbval 16298 mplmonmul 18743 regr1lem 20809 blcld 21575 stdbdxmet 21585 itgss 22825 isosctrlem2 23804 isppw2 24098 dchrelbas3 24222 lgsdir 24314 rplogsum 24421 nb3graprlem2 25236 orngsqr 28618 qqhval2lem 28836 qqhf 28841 esumpinfval 28945 bj-dtru 31458 poimirlem24 32010 isfldidl 32347 lssat 32628 paddasslem1 33431 lcfrlem21 35177 hdmap10lem 35456 hdmap11lem2 35459 jm2.23 35897 cncfiooicclem1 37857 fourierdlem81 38152 2f1fvneq 39150 nb3grprlem2 39601 |
Copyright terms: Public domain | W3C validator |