![]() |
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 8701 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 2 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1463 ℂcc 7545 2c2 8681 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-11 1467 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-resscn 7637 ax-1re 7639 ax-addrcl 7642 |
This theorem depends on definitions: df-bi 116 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-in 3043 df-ss 3050 df-2 8689 |
This theorem is referenced by: cnm2m1cnm3 8875 xp1d2m1eqxm1d2 8876 nneo 9058 zeo2 9061 2tnp1ge0ge0 9967 flhalf 9968 q2txmodxeq0 10050 mulbinom2 10301 binom3 10302 zesq 10303 sqoddm1div8 10337 cvg1nlemcxze 10646 resqrexlemover 10674 resqrexlemlo 10677 resqrexlemcalc1 10678 resqrexlemnm 10682 amgm2 10782 maxabslemab 10870 maxabslemlub 10871 max0addsup 10883 minabs 10899 bdtri 10903 trirecip 11162 geo2sum 11175 ege2le3 11228 efgt0 11241 tanval3ap 11272 even2n 11419 oddm1even 11420 oddp1even 11421 mulsucdiv2z 11430 ltoddhalfle 11438 m1exp1 11446 nn0enne 11447 flodddiv4 11479 flodddiv4t2lthalf 11482 sqrt2irrlem 11685 sqrt2irr 11686 pw2dvdslemn 11688 pw2dvdseulemle 11690 oddpwdc 11697 sqrt2irraplemnn 11702 oddennn 11750 evenennn 11751 cvgcmp2nlemabs 12919 trilpolemisumle 12923 |
Copyright terms: Public domain | W3C validator |