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

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

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 7986 . 2
21a1i 9 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 1393  cc 6887  c2 7964 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6976  ax-1re 6978  ax-addrcl 6981 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931  df-2 7973 This theorem is referenced by:  cnm2m1cnm3  8176  nneo  8341  zeo2  8344  2tnp1ge0ge0  9143  flhalf  9144  binom3  9366  zesq  9367  cvg1nlemcxze  9581  resqrexlemover  9608  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemnm  9616  amgm2  9714  sqr2irrlem  9877  sqrt2irr  9878
 Copyright terms: Public domain W3C validator