Theorem 2cnd 9179

Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2cnd	⊢ (𝜑 → 2 ∈ ℂ)

Proof of Theorem 2cnd

Step	Hyp	Ref	Expression
1		2cn 9177	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 2 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 7993  2c2 9157

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9165

This theorem is referenced by:  subhalfhalf  9342  cnm2m1cnm3  9359  xp1d2m1eqxm1d2  9360  nneo  9546  zeo2  9549  2tnp1ge0ge0  10516  flhalf  10517  fldiv4lem1div2uz2  10521  q2txmodxeq0  10601  mulbinom2  10873  binom3  10874  zesq  10875  sqoddm1div8  10910  mulsubdivbinom2ap  10928  cvg1nlemcxze  11488  resqrexlemover  11516  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemnm  11524  amgm2  11624  maxabslemab  11712  maxabslemlub  11713  max0addsup  11725  minabs  11742  bdtri  11746  trirecip  12007  geo2sum  12020  ege2le3  12177  efgt0  12190  tanval3ap  12220  even2n  12380  oddm1even  12381  oddp1even  12382  mulsucdiv2z  12391  ltoddhalfle  12399  m1exp1  12407  nn0enne  12408  flodddiv4  12442  flodddiv4t2lthalf  12445  bitsp1e  12458  bitsp1o  12459  bitsmod  12462  bitsinv1lem  12467  sqrt2irrlem  12678  sqrt2irr  12679  pw2dvdslemn  12682  pw2dvdseulemle  12684  oddpwdc  12691  sqrt2irraplemnn  12696  prmdiv  12752  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  4sqlem7  12902  4sqlem10  12905  4sqlem19  12927  2expltfac  12957  oddennn  12958  evenennn  12959  hoverb  15316  sin0pilem2  15450  perfectlem2  15668  perfect  15669  lgslem1  15673  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem3  15736  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  2lgslem1a1  15759  2lgslem1a2  15760  2lgslem1b  15762  2lgslem1c  15763  2lgslem3a1  15770  2lgslem3d1  15773  cvgcmp2nlemabs  16359  trilpolemisumle  16365  apdifflemr  16374  apdiff  16375