Theorem 2cnd 9108

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 9106	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 2 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  2c2 9086

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-2 9094

This theorem is referenced by:  subhalfhalf  9271  cnm2m1cnm3  9288  xp1d2m1eqxm1d2  9289  nneo  9475  zeo2  9478  2tnp1ge0ge0  10442  flhalf  10443  fldiv4lem1div2uz2  10447  q2txmodxeq0  10527  mulbinom2  10799  binom3  10800  zesq  10801  sqoddm1div8  10836  mulsubdivbinom2ap  10854  cvg1nlemcxze  11264  resqrexlemover  11292  resqrexlemlo  11295  resqrexlemcalc1  11296  resqrexlemnm  11300  amgm2  11400  maxabslemab  11488  maxabslemlub  11489  max0addsup  11501  minabs  11518  bdtri  11522  trirecip  11783  geo2sum  11796  ege2le3  11953  efgt0  11966  tanval3ap  11996  even2n  12156  oddm1even  12157  oddp1even  12158  mulsucdiv2z  12167  ltoddhalfle  12175  m1exp1  12183  nn0enne  12184  flodddiv4  12218  flodddiv4t2lthalf  12221  bitsp1e  12234  bitsp1o  12235  bitsmod  12238  bitsinv1lem  12243  sqrt2irrlem  12454  sqrt2irr  12455  pw2dvdslemn  12458  pw2dvdseulemle  12460  oddpwdc  12467  sqrt2irraplemnn  12472  prmdiv  12528  pythagtriplem15  12572  pythagtriplem16  12573  pythagtriplem17  12574  4sqlem7  12678  4sqlem10  12681  4sqlem19  12703  2expltfac  12733  oddennn  12734  evenennn  12735  hoverb  15091  sin0pilem2  15225  perfectlem2  15443  perfect  15444  lgslem1  15448  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem3  15511  gausslemma2dlem6  15515  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  2lgslem1a1  15534  2lgslem1a2  15535  2lgslem1b  15537  2lgslem1c  15538  2lgslem3a1  15545  2lgslem3d1  15548  cvgcmp2nlemabs  15933  trilpolemisumle  15939  apdifflemr  15948  apdiff  15949