![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2cnd | GIF version |
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
2cnd | ⊢ (𝜑 → 2 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 9004 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 2 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2158 ℂcc 7823 2c2 8984 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-resscn 7917 ax-1re 7919 ax-addrcl 7922 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-in 3147 df-ss 3154 df-2 8992 |
This theorem is referenced by: cnm2m1cnm3 9184 xp1d2m1eqxm1d2 9185 nneo 9370 zeo2 9373 2tnp1ge0ge0 10315 flhalf 10316 q2txmodxeq0 10398 mulbinom2 10651 binom3 10652 zesq 10653 sqoddm1div8 10688 mulsubdivbinom2ap 10705 cvg1nlemcxze 11005 resqrexlemover 11033 resqrexlemlo 11036 resqrexlemcalc1 11037 resqrexlemnm 11041 amgm2 11141 maxabslemab 11229 maxabslemlub 11230 max0addsup 11242 minabs 11258 bdtri 11262 trirecip 11523 geo2sum 11536 ege2le3 11693 efgt0 11706 tanval3ap 11736 even2n 11893 oddm1even 11894 oddp1even 11895 mulsucdiv2z 11904 ltoddhalfle 11912 m1exp1 11920 nn0enne 11921 flodddiv4 11953 flodddiv4t2lthalf 11956 sqrt2irrlem 12175 sqrt2irr 12176 pw2dvdslemn 12179 pw2dvdseulemle 12181 oddpwdc 12188 sqrt2irraplemnn 12193 prmdiv 12249 pythagtriplem15 12292 pythagtriplem16 12293 pythagtriplem17 12294 4sqlem7 12396 4sqlem10 12399 oddennn 12407 evenennn 12408 sin0pilem2 14556 lgslem1 14754 lgseisenlem1 14803 lgseisenlem2 14804 cvgcmp2nlemabs 15134 trilpolemisumle 15140 apdifflemr 15149 apdiff 15150 |
Copyright terms: Public domain | W3C validator |