ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2cnd Unicode version

Theorem 2cnd 9057
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
2cnd  |-  ( ph  ->  2  e.  CC )

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 9055 . 2  |-  2  e.  CC
21a1i 9 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2164   CCcc 7872   2c2 9035
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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167  df-2 9043
This theorem is referenced by:  subhalfhalf  9220  cnm2m1cnm3  9237  xp1d2m1eqxm1d2  9238  nneo  9423  zeo2  9426  2tnp1ge0ge0  10373  flhalf  10374  fldiv4lem1div2uz2  10378  q2txmodxeq0  10458  mulbinom2  10730  binom3  10731  zesq  10732  sqoddm1div8  10767  mulsubdivbinom2ap  10785  cvg1nlemcxze  11129  resqrexlemover  11157  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemnm  11165  amgm2  11265  maxabslemab  11353  maxabslemlub  11354  max0addsup  11366  minabs  11382  bdtri  11386  trirecip  11647  geo2sum  11660  ege2le3  11817  efgt0  11830  tanval3ap  11860  even2n  12018  oddm1even  12019  oddp1even  12020  mulsucdiv2z  12029  ltoddhalfle  12037  m1exp1  12045  nn0enne  12046  flodddiv4  12078  flodddiv4t2lthalf  12081  sqrt2irrlem  12302  sqrt2irr  12303  pw2dvdslemn  12306  pw2dvdseulemle  12308  oddpwdc  12315  sqrt2irraplemnn  12320  prmdiv  12376  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  4sqlem7  12525  4sqlem10  12528  4sqlem19  12550  oddennn  12552  evenennn  12553  hoverb  14827  sin0pilem2  14958  lgslem1  15157  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem3  15220  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1b  15246  2lgslem1c  15247  2lgslem3a1  15254  2lgslem3d1  15257  cvgcmp2nlemabs  15592  trilpolemisumle  15598  apdifflemr  15607  apdiff  15608
  Copyright terms: Public domain W3C validator