MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recnd Unicode version

Theorem recnd 8863
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
recnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem recnd
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 recn 8829 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 15 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   CCcc 8737   RRcr 8738
This theorem is referenced by:  00id  8989  mul02lem1  8990  addid1  8994  cnegex  8995  ltadd1  9243  leadd2  9245  ltsubadd  9246  ltsubadd2  9247  lesubadd  9248  lesubadd2  9249  lesub1  9270  lesub2  9271  ltnegcon1  9277  ltnegcon2  9278  add20  9288  subge0  9289  suble0  9290  lesub0  9292  mulge0  9293  eqord2  9306  rereccl  9480  redivcl  9481  recgt0  9602  prodgt0  9603  prodge0  9605  ltmul1a  9607  ltdiv1  9622  ltmuldiv  9628  ltrec  9639  recp1lt1  9656  recreclt  9657  ledivp1  9660  infmsup  9734  infmrcl  9735  rimul  9739  cru  9740  avglt1  9951  avglt2  9952  nn0cnd  10022  zcn  10031  zeo  10099  zcnd  10120  cnref1o  10351  rpcn  10364  rpcnd  10394  ltaddrp2d  10422  qbtwnre  10528  xralrple  10534  xpncan  10573  xmulcom  10588  xmulneg1  10591  xlemul1  10612  icoshftf1o  10761  lincmb01cmp  10779  iccf1o  10780  fladdz  10952  flzadd  10953  flhalf  10956  ceim1l  10959  intfracq  10965  fldiv  10966  mod0  10980  modlt  10983  moddiffl  10984  modfrac  10986  flmod  10987  intfrac  10988  modmulnn  10990  modid  10995  modcyc  11001  modadd1  11003  modnegd  11006  modadd12d  11007  modsub12d  11008  moddi  11009  modsubdir  11010  modirr  11011  seqf1olem1  11087  serle  11103  expcl2lem  11117  expnegz  11138  expaddzlem  11147  expaddz  11148  expmulz  11150  ltexp2a  11155  leexp2a  11159  leexp2r  11161  exple1  11163  expubnd  11164  sq11  11178  bernneq2  11230  expmulnbnd  11235  discr1  11239  discr  11240  faclbnd  11305  bcp1nk  11331  remim  11604  reim0b  11606  rereb  11607  mulre  11608  cjreb  11610  recj  11611  reneg  11612  readd  11613  resub  11614  remullem  11615  remul2  11617  rediv  11618  imcj  11619  imneg  11620  imadd  11621  imsub  11622  immul2  11624  imdiv  11625  cjcj  11627  cjadd  11628  ipcnval  11630  cjmulval  11632  cjneg  11634  imval2  11638  cjreim2  11648  sqr0lem  11728  sqrlem5  11734  sqrlem7  11736  resqrthlem  11742  remsqsqr  11744  sqrmul  11747  sqrdiv  11753  sqrneg  11755  sqrmsq  11758  absdiv  11782  absid  11783  absexp  11791  absexpz  11792  absimle  11796  abslt  11800  absle  11801  abssubne0  11802  releabs  11807  recval  11808  abstri  11816  abs2difabs  11820  abs1m  11821  abslem2  11825  absrdbnd  11827  sqreulem  11845  sqreu  11846  amgm2  11855  lo1bddrp  12001  o1lo1  12013  rlimrecl  12056  rlimge0  12057  climrecl  12059  climge0  12060  climabs0  12061  reccn2  12072  o1rlimmul  12094  lo1mul2  12104  lo1sub  12106  climle  12115  climsqz  12116  climsqz2  12117  rlimsqz  12125  rlimsqz2  12126  rlimno1  12129  climlec2  12134  isercolllem1  12140  climsup  12145  caucvgrlem  12147  caurcvgr  12148  caucvgrlem2  12149  iseraltlem1  12156  iseraltlem2  12157  iseraltlem3  12158  iseralt  12159  isumrecl  12230  isumge0  12231  fsumless  12256  fsumge1  12257  fsum00  12258  fsumle  12259  fsumlt  12260  fsumabs  12261  o1fsum  12273  seqabs  12274  cvgcmp  12276  cvgcmpce  12278  abscvgcvg  12279  isumrpcl  12304  isumle  12305  isumless  12306  isumsup  12308  climcndslem1  12310  climcndslem2  12311  climcnds  12312  flo1  12315  supcvg  12316  trireciplem  12322  trirecip  12323  explecnv  12325  geo2sum  12331  geo2lim  12333  geomulcvg  12334  cvgrat  12341  mertenslem1  12342  mertenslem2  12343  efcllem  12361  ege2le3  12373  efaddlem  12376  efgt0  12385  eftlub  12391  effsumlt  12393  eflt  12399  eflegeo  12403  resin4p  12420  recos4p  12421  retanhcl  12441  tanhlt1  12442  efeul  12444  ef01bndlem  12466  sin01bnd  12467  cos01bnd  12468  sin01gt0  12472  cos01gt0  12473  sin02gt0  12474  absefi  12478  absef  12479  absefib  12480  efieq1re  12481  eirrlem  12484  rpnnen2lem5  12499  rpnnen2lem8  12502  rpnnen2lem9  12503  rpnnen2lem11  12505  rpnnen2  12506  moddvds  12540  odd2np1  12589  divalglem5  12598  bitsp1  12624  bitsp1o  12626  bitsfzo  12628  bitscmp  12631  sadcaddlem  12650  nn0seqcvgd  12742  sqnprm  12779  isprm5  12793  nonsq  12832  eulerthlem2  12852  prmdiveq  12856  odzdvds  12862  pythagtriplem14  12883  pcid  12927  fldivp1  12947  pcfac  12949  pockthlem  12954  prmreclem3  12967  prmreclem4  12968  prmreclem5  12969  prmrec  12971  4sqlem5  12991  4sqlem10  12996  mul4sqlem  13002  4sqlem15  13008  4sqlem16  13009  mulgneg  14587  ghmmulg  14697  odmodnn0  14857  mndodconglem  14858  pgpfaclem2  15319  isabvd  15587  abv1z  15599  abvneg  15601  abvrec  15603  abvdiv  15604  abvdom  15605  rege0subm  16430  cnsubrg  16434  gzrngunitlem  16438  prmirredlem  16448  bl2in  17959  blhalf  17962  blss  17974  methaus  18068  nrmmetd  18099  nm2dif  18148  nminvr  18182  nmdvr  18183  nlmmul0or  18196  nrginvrcnlem  18203  nmolb2d  18229  nmoi2  18241  nmoleub  18242  nmo0  18246  nmoeq0  18247  nmoco  18248  nmotri  18250  nmoid  18253  blcvx  18306  xrsxmet  18317  recld2  18322  reconnlem2  18334  opnreen  18338  metdstri  18357  metnrmlem3  18367  iihalf2cn  18434  icchmeo  18441  icopnfcnv  18442  icopnfhmeo  18443  iccpnfhmeo  18445  xrhmeo  18446  icccvx  18450  cnheiborlem  18454  evth  18459  lebnumii  18466  pcoass  18524  pcorevlem  18526  pcorev2  18528  pi1xfrcnv  18557  nmoleub2lem  18597  nmoleub2lem3  18598  nmoleub3  18602  cphsqrcl2  18624  ipcau2  18666  tchcphlem1  18667  tchcphlem2  18668  tchcph  18669  iscau3  18706  minveclem2  18792  minveclem3b  18794  minveclem4  18798  minveclem6  18800  minveclem7  18801  pjthlem1  18803  ivthlem2  18814  ivthlem3  18815  ivth2  18817  ovolfsval  18832  ovollb2lem  18849  ovolctb  18851  ovolunlem1a  18857  ovolunnul  18861  ovolfiniun  18862  ovoliunlem1  18863  ovoliun2  18867  shft2rab  18869  ovolshftlem1  18870  sca2rab  18873  ovolscalem1  18874  ovolsca  18876  ovolicc1  18877  ovolicc2lem4  18881  ovolicopnf  18885  cmmbl  18894  nulmbl  18895  nulmbl2  18896  unmbl  18897  volinun  18905  volfiniun  18906  voliunlem1  18909  voliunlem3  18911  ioombl1lem3  18919  ioombl1lem4  18920  ovolioo  18927  ioorcl2  18929  uniioovol  18936  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombllem6  18945  dyadovol  18950  dyaddisjlem  18952  opnmbllem  18958  vitalilem1  18965  vitalilem2  18966  vitalilem3  18967  vitalilem4  18968  ismbf  18987  mbfmulc2lem  19004  mbfmulc2re  19005  mbfpos  19008  mbfmulc2  19020  mbfinf  19022  itg1val2  19041  itg11  19048  i1fmullem  19051  i1fadd  19052  itg1addlem4  19056  itg1addlem5  19057  i1fmulclem  19059  i1fmulc  19060  itg1mulc  19061  itg1sub  19066  itg10a  19067  itg1ge0a  19068  itg1climres  19071  mbfi1fseqlem3  19074  mbfi1fseqlem4  19075  mbfi1fseqlem5  19076  mbfi1fseqlem6  19077  mbfi1flimlem  19079  mbfmullem2  19081  itg2const  19097  itg2const2  19098  itg2mulclem  19103  itg2mulc  19104  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  itg2monolem3  19109  itg2addlem  19115  itgcl  19140  itgcnlem  19146  itgrevallem1  19151  itgposval  19152  iblneg  19159  itgneg  19160  i1fibl  19164  itgitg1  19165  itgconst  19175  ibladd  19177  itgaddlem2  19180  iblabslem  19184  iblabs  19185  iblabsr  19186  iblmulc2  19187  itgmulc2lem2  19189  itgmulc2  19190  itgabs  19191  itgsplit  19192  bddmulibl  19195  dvcjbr  19300  dvfre  19302  dvexp3  19327  dveflem  19328  dvferm1lem  19333  dvferm2lem  19335  rolle  19339  cmvth  19340  mvth  19341  dvlip  19342  dvlipcn  19343  c1liplem1  19345  c1lip1  19346  dveq0  19349  dv11cn  19350  dvlt0  19354  dvle  19356  dvivthlem1  19357  dvivth  19359  lhop1lem  19362  lhop1  19363  lhop2  19364  lhop  19365  dvcvx  19369  dvfsumle  19370  dvfsumge  19371  dvfsumabs  19372  dvfsumlem1  19375  dvfsumlem2  19376  dvfsumlem4  19378  dvfsumrlimge0  19379  dvfsumrlim2  19381  dvfsum2  19383  ftc1a  19386  ftc1lem4  19388  ftc1lem5  19389  plyeq0lem  19594  coemulhi  19637  plyrecj  19662  plydivlem3  19677  aalioulem2  19715  aalioulem3  19716  aalioulem4  19717  aalioulem5  19718  aalioulem6  19719  aaliou  19720  aaliou2  19722  aaliou2b  19723  aaliou3lem3  19726  aaliou3lem7  19731  aaliou3lem9  19732  taylthlem2  19755  ulmcn  19778  ulmdvlem1  19779  mtest  19783  itgulm  19786  radcnvlem1  19791  radcnvlem2  19792  radcnvlt1  19796  radcnvle  19798  dvradcnv  19799  pserulm  19800  abelthlem2  19810  abelthlem5  19813  abelthlem7  19816  abelth2  19820  reeff1olem  19824  efcvx  19827  pilem2  19830  pilem3  19831  sincosq2sgn  19869  sincosq3sgn  19870  sincosq4sgn  19871  coseq0negpitopi  19873  tanrpcl  19874  tangtx  19875  tanabsge  19876  sinq12gt0  19877  sinq34lt0t  19879  cosq14gt0  19880  cosq14ge0  19881  pige3  19887  coskpi  19890  sineq0  19891  cosordlem  19895  sinord  19898  tanord1  19901  tanord  19902  tanregt0  19903  efif1olem2  19907  efif1olem4  19909  eff1olem  19912  logrnaddcl  19933  logneg  19943  lognegb  19945  reexplog  19950  relogexp  19951  logfac  19956  efiarg  19963  cosargd  19964  cosarg0d  19965  argregt0  19966  argrege0  19967  argimgt0  19968  logneg2  19971  tanarg  19972  logdivlti  19973  divlogrlim  19984  logcnlem2  19992  logcnlem3  19993  logcnlem4  19994  logcn  19996  logf1o2  19999  advlog  20003  advlogexp  20004  efopnlem1  20005  logtayllem  20008  logtayl  20009  logccv  20012  logcxp  20018  mulcxp  20034  divcxp  20036  cxpmul  20037  cxproot  20039  cxpmul2z  20040  abscxp  20041  abscxp2  20042  cxplt  20043  cxplea  20045  cxple2  20046  cxple2a  20048  cxplt3  20049  cxpsqrlem  20051  cxpsqr  20052  logsqr  20053  dvcxp2  20085  cxpcn3lem  20089  resqrcn  20091  cxpaddlelem  20093  cxpaddle  20094  abscxpbnd  20095  root1id  20096  root1eq1  20097  root1cj  20098  cxpeq  20099  loglesqr  20100  cosangneg2d  20107  angrtmuld  20108  ang180lem2  20110  lawcoslem1  20115  lawcos  20116  pythag  20117  isosctrlem1  20120  isosctrlem2  20121  isosctrlem3  20122  ssscongptld  20124  chordthmlem  20131  chordthmlem2  20132  chordthmlem3  20133  chordthmlem4  20134  chordthmlem5  20135  asinsinlem  20189  reasinsin  20194  acosrecl  20201  atancj  20208  atanrecl  20209  atanlogaddlem  20211  atanlogsublem  20213  atanbndlem  20223  atans2  20229  ressatans  20232  atantayl  20235  leibpilem2  20239  leibpi  20240  leibpisum  20241  log2tlbnd  20243  log2ublem2  20245  birthdaylem2  20249  birthdaylem3  20250  cxp2limlem  20272  cxp2lim  20273  cxploglim  20274  cxploglim2  20275  divsqrsumo1  20280  cvxcl  20281  scvxcvx  20282  jensenlem2  20284  jensen  20285  amgmlem  20286  emcllem2  20292  emcllem3  20293  emcllem5  20295  emcllem6  20296  emcllem7  20297  harmonicbnd4  20306  fsumharmonic  20307  ftalem1  20312  ftalem2  20313  ftalem4  20315  ftalem5  20316  basellem3  20322  basellem4  20323  basellem5  20324  basellem6  20325  basellem7  20326  basellem8  20327  basellem9  20328  efnnfsumcl  20342  chtprm  20393  chpp1  20395  chtdif  20398  efchtdvds  20399  prmorcht  20418  mumullem2  20420  fsumfldivdiaglem  20431  ppiub  20445  chtleppi  20451  chtublem  20452  chtub  20453  pclogsum  20456  vmasum  20457  logfac2  20458  chpval2  20459  chpchtsum  20460  chpub  20461  logfaclbnd  20463  logfacbnd3  20464  logfacrlim  20465  logexprlim  20466  logfacrlim2  20467  mersenne  20468  dchrabs  20501  dchrptlem1  20505  dchrptlem2  20506  bcmax  20519  bcp1ctr  20520  bposlem1  20525  bposlem9  20533  lgsvalmod  20556  lgsdilem  20563  lgsne0  20574  lgsqrlem2  20583  lgseisenlem1  20590  lgseisenlem2  20591  lgseisen  20594  lgsquadlem1  20595  lgsquadlem2  20596  mul2sq  20606  2sqlem3  20607  2sqlem8  20613  chebbnd1lem1  20620  chebbnd1lem2  20621  chebbnd1lem3  20622  chtppilimlem1  20624  chtppilimlem2  20625  chtppilim  20626  chto1ub  20627  chto1lb  20629  chpchtlim  20630  chpo1ub  20631  vmadivsum  20633  vmadivsumb  20634  rplogsumlem1  20635  rplogsumlem2  20636  rpvmasumlem  20638  dchrisumlema  20639  dchrisumlem1  20640  dchrisumlem2  20641  dchrisumlem3  20642  dchrmusumlema  20644  dchrmusum2  20645  dchrvmasumlem1  20646  dchrvmasum2lem  20647  dchrvmasum2if  20648  dchrvmasumlem2  20649  dchrvmasumlem3  20650  dchrvmasumiflem1  20652  dchrvmasumiflem2  20653  dchrisum0flblem1  20659  dchrisum0fno1  20662  rpvmasum2  20663  dchrisum0re  20664  dchrisum0lema  20665  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2a  20668  dchrisum0lem2  20669  dchrisum0lem3  20670  dchrmusumlem  20673  dchrvmasumlem  20674  rpvmasum  20677  rplogsum  20678  dirith2  20679  mudivsum  20681  mulogsumlem  20682  mulogsum  20683  logdivsum  20684  mulog2sumlem1  20685  mulog2sumlem2  20686  mulog2sumlem3  20687  vmalogdivsum2  20689  vmalogdivsum  20690  2vmadivsumlem  20691  logsqvma  20693  logsqvma2  20694  log2sumbnd  20695  selberglem1  20696  selberglem2  20697  selberglem3  20698  selberg  20699  selbergb  20700  selberg2lem  20701  selberg2  20702  selberg2b  20703  chpdifbndlem1  20704  logdivbnd  20707  selberg3lem1  20708  selberg3lem2  20709  selberg3  20710  selberg4lem1  20711  selberg4  20712  pntrmax  20715  pntrsumo1  20716  pntrsumbnd  20717  pntrsumbnd2  20718  selbergr  20719  selberg3r  20720  selberg4r  20721  selberg34r  20722  pntsval2  20727  pntrlog2bndlem1  20728  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bndlem6a  20733  pntrlog2bndlem6  20734  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd1  20737  pntpbnd2  20738  pntibndlem2  20742  pntibndlem3  20743  pntlemb  20748  pntlemg  20749  pntlemh  20750  pntlemn  20751  pntlemr  20753  pntlemj  20754  pntlemf  20756  pntlemk  20757  pntlemo  20758  pntlem3  20760  pntleml  20762  pnt2  20764  pnt  20765  abvcxp  20766  ostth2lem1  20769  qabvexp  20777  padicabv  20781  padicabvcxp  20783  ostth2lem2  20785  ostth2lem3  20786  ostth2lem4  20787  ostth2  20788  ostth3  20789  nvm1  21232  nvpi  21234  nvz0  21236  nvmtri  21239  nvabs  21241  nvge0  21242  nv1  21244  smcnlem  21272  ipval2lem4  21281  ipval2  21282  4ipval2  21283  4ipval3  21287  ipidsq  21288  dipcj  21292  dip0r  21295  ipz  21297  nmoub3i  21353  nmlno0lem  21373  nmblolbii  21379  blocnilem  21384  cncph  21399  ipasslem4  21414  ipasslem5  21415  ipblnfi  21436  minvecolem2  21456  minvecolem4  21461  minvecolem6  21463  minvecolem7  21464  htthlem  21499  normpyc  21727  hhph  21759  bcs2  21763  norm1  21830  norm1exi  21831  pjhthlem1  21972  eigvalcl  22543  eighmorth  22546  nmlnop0iALT  22577  nmbdoplbi  22606  nmcexi  22608  nmcoplbi  22610  nmbdfnlbi  22631  nmcfnlbi  22634  riesz4i  22645  cnlnadjlem2  22650  cnlnadjlem7  22655  nmopcoi  22677  nmopcoadji  22683  branmfn  22687  leopnmid  22720  opsqrlem1  22722  hst1h  22809  hstle  22812  hstoh  22814  sto2i  22819  stadd3i  22830  strlem1  22832  golem1  22853  stcltrlem1  22858  cdj1i  23015  cdj3lem1  23016  cdj3lem3b  23022  cdj3i  23023  fzsplit3  23033  bcm1n  23034  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsgt1  23071  ballotlemsel1i  23073  ballotlemsi  23075  lt2addrd  23251  sqsscirc1  23294  sqsscirc2  23295  cnre2csqima  23297  rmulccn  23303  xrge0iifcnv  23317  xrge0iifhom  23321  nnlogbexp  23408  logbrec  23409  esumpcvgval  23448  dya2ub  23577  dya2iocseg  23581  indsum  23608  zetacvg  23691  subfacval2  23720  subfaclim  23721  subfacval3  23722  rescon  23779  eupap1  23902  sinccvglem  24007  circum  24009  modaddabs  24013  fveecn  24532  eqeelen  24534  brbtwn2  24535  colinearalglem4  24539  colinearalg  24540  axsegconlem9  24555  axsegconlem10  24556  ax5seglem1  24558  ax5seglem2  24559  ax5seglem3  24561  ax5seglem5  24563  ax5seglem6  24564  ax5seglem9  24567  ax5seg  24568  axbtwnid  24569  axpaschlem  24570  axpasch  24571  axeuclidlem  24592  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  axcontlem8  24601  bpolydiflem  24791  bpoly4  24796  dvreasin  24925  dvreacos  24926  supadd  24928  ltflcei  24930  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  areacirclem2  24936  areacirclem3  24937  areacirclem6  24941  areacirc  24942  cntrset  25613  dmse1  25614  msr3  25616  msr4  25617  mslb1  25618  2wsms  25619  msra3  25620  iintlem1  25621  lvsovso  25637  rnegvex2  25672  nn0prpwlem  26249  csbrn  26473  trirn  26474  mettrifi  26484  lmclim2  26485  geomcau  26486  isbnd3  26519  ssbnd  26523  cntotbnd  26531  bfplem1  26557  bfplem2  26558  bfp  26559  rrnmet  26564  rrndstprj1  26565  rrndstprj2  26566  rrncmslem  26567  rrnequiv  26570  rrntotbnd  26571  ismrer1  26573  eldioph2lem1  26850  lzenom  26860  rencldnfilem  26914  icodiamlt  26916  irrapxlem1  26918  irrapxlem2  26919  irrapxlem3  26920  irrapxlem4  26921  irrapxlem5  26922  pellexlem2  26926  pellexlem6  26930  pell1234qrreccl  26950  pell14qrgt0  26955  pell14qrdivcl  26961  pell14qrexpclnn0  26962  pell14qrexpcl  26963  pell14qrdich  26965  pell1qrgaplem  26969  pellfundex  26982  reglogmul  26989  reglogexp  26990  reglogbas  26991  reglog1  26992  pellfund14  26994  rmspecsqrnq  27002  rmspecfund  27005  rmym1  27031  rmyluc  27033  monotoddzzfi  27038  expmordi  27043  jm2.24nn  27057  jm2.17a  27058  jm2.17b  27059  jm2.17c  27060  jm2.24  27061  acongrep  27078  fzmaxdif  27079  acongeq  27081  modabsdifz  27089  jm2.19lem4  27096  jm2.19  27097  jm2.26lem3  27105  jm3.1lem1  27121  jm3.1lem2  27122  dvconstbi  27562  climinf  27743  stoweidlem13  27773  stoweidlem17  27777  stoweidlem21  27781  stoweidlem47  27807  stoweidlem59  27819  wallispilem3  27827  wallispilem5  27829  wallispi2lem1  27831  stirlinglem1  27834  stirlinglem5  27838  stirlinglem11  27844  stirlinglem12  27845  stirlinglem14  27847  sigaras  27856  sigarms  27857  sigarls  27858  sigarexp  27860  sigarperm  27861  sigarimcd  27863  sigarcol  27865  sharhght  27866  cevathlem2  27869
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-resscn 8796
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator