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

Theorem eqeq12d 2310
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1  |-  ( ph  ->  A  =  B )
eqeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eqeq12d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 eqeq12 2308 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632
This theorem is referenced by:  cdeqeq  2999  sbceqg  3110  csbing  3389  csbifg  3606  uniprg  3858  unisng  3860  intprg  3912  iununi  4002  csbopabg  4110  limeq  4420  ordunisuc  4639  onsucuni2  4641  orduninsuc  4650  csbima12g  5038  dmsnsnsn  5167  cnvsng  5174  csbiotag  5264  csbfv12gALT  5552  fveqres  5576  fvmptf  5632  eqfnfv2f  5642  fvreseq  5644  fmptco  5707  fnressn  5721  fvsng  5730  fnsuppres  5748  cocan1  5817  cocan2  5818  fliftfun  5827  weniso  5868  csbovg  5905  eqfnov  5966  ovmpt2s  5987  ov2gf  5988  ovmpt2dxf  5989  caovcomg  6031  caovassg  6034  caovcang  6037  caovcanrd  6039  caovcan  6040  caovdig  6050  caovdirg  6053  caovmo  6073  grprinvlem  6074  grprinvd  6075  offveqb  6115  caofid0l  6121  caofid0r  6122  caofass  6127  caonncan  6131  op1stg  6148  op2ndg  6149  opabiota  6309  csbriotag  6333  onfununi  6374  tfrlem1  6407  tfrlem2  6408  tfrlem3  6409  tfrlem3a  6410  tfrlem9  6417  tfrlem11  6420  tfrlem12  6421  tfr3  6431  tz7.44-1  6435  tz7.44-2  6436  tz7.44-3  6437  rdglem1  6444  rdg0g  6456  seqomlem1  6478  abianfp  6487  oalim  6547  omlim  6548  oelim  6549  oa0r  6553  om0r  6554  om1r  6557  oaass  6575  oarec  6576  odi  6593  omass  6594  oelim2  6609  oeoalem  6610  oeoa  6611  oeoelem  6612  oeoe  6613  nna0r  6623  nnacom  6631  nnaass  6636  nndi  6637  nnmass  6638  nnmsucr  6639  nnmcom  6640  oaabs  6658  oaabs2  6659  omabs  6661  ecovcom  6785  ecovass  6786  ecovdi  6787  dom2lem  6917  unxpdomlem2  7084  unxpdomlem3  7085  ixpfi2  7170  fipreima  7177  ordiso2  7246  wemaplem1  7277  wemaplem2  7278  wemapso2lem  7281  cantnfval2  7386  cantnfp1lem3  7398  oemapvali  7402  cantnflem1c  7405  cantnflem1  7407  wemapwe  7416  tcvalg  7439  rankvalg  7505  rankonidlem  7516  ranklim  7532  rankuni  7551  cardprclem  7628  cardprc  7629  carduni  7630  fseqenlem1  7667  fodomacn  7699  alephcard  7713  alephfp2  7752  alephval3  7753  dfac12lem1  7785  dfac12lem2  7786  dfac12r  7788  ackbij1lem5  7866  ackbij1lem8  7869  ackbij1lem14  7875  ackbij1lem16  7877  ackbij2lem3  7883  cardcf  7894  sornom  7919  fin23lem28  7982  isf32lem2  7996  itunitc  8063  ituniiun  8064  axdc3lem2  8093  axdc4lem  8097  ttukeylem3  8154  ttukey2g  8159  fpwwe2lem8  8275  fpwwecbv  8282  canth4  8285  pwfseqlem2  8297  addcanpi  8539  mulcanpi  8540  recrecnq  8607  ltexnq  8615  genpv  8639  0idsr  8735  1idsr  8736  ax1rid  8799  mulid1  8851  addcan  9012  addcan2  9013  mulcand  9417  mulcan2d  9418  div11  9466  divmuleq  9481  conjmul  9493  eqneg  9496  ofsubeq0  9759  rpnnen1  10363  cnref1o  10365  xmulasslem  10621  xmulass  10623  xadddi2  10633  prunioo  10780  fzsuc2  10858  fzprval  10860  fztpval  10861  modadd1  11017  modmul1  11018  om2uzsuci  11027  om2uzrdg  11035  uzrdgxfr  11045  seq1  11075  seqp1  11077  seqfveq2  11084  seqfveq  11086  seqshft2  11088  seqsplit  11095  seqcaopr3  11097  seqcaopr2  11098  seqf1olem2a  11100  seqf1olem2  11102  seqf1o  11103  seqid  11107  seqid2  11108  seqhomo  11109  ser1const  11118  mulexp  11157  expadd  11160  expmul  11163  binom2  11234  sq01  11239  modexp  11252  bcpasc  11349  hashgadd  11375  hashdom  11377  hashfzo  11399  hashxplem  11401  hashxp  11402  hashmap  11403  hashpw  11404  hashbclem  11406  hashbc  11407  hashfacen  11408  hashf1lem1  11409  hashf1lem2  11410  hashf1  11411  seqcoll  11417  ccatopth  11478  ccatopth2  11479  cats1un  11492  replim  11617  cjreb  11624  cjexp  11651  absexp  11805  abs1m  11835  recan  11836  isercoll2  12158  iseraltlem2  12171  iseraltlem3  12172  sumeq2w  12181  sumeq2ii  12182  zsum  12207  fsum  12209  fsumf1o  12212  sumss  12213  fsumcvg2  12216  fsumadd  12227  isummulc2  12241  fsum2d  12250  fsummulc2  12262  fsumconst  12268  fsumparts  12280  fsumrelem  12281  fsumiun  12295  binom  12304  bcxmas  12310  incexclem  12311  isumshft  12314  isumnn0nn  12317  climcndslem1  12324  climcndslem2  12325  mertenslem2  12357  efne0  12393  efexp  12397  demoivreALT  12497  moddvds  12554  bitsinv1  12649  sadadd2  12667  smu01lem  12692  smupval  12695  smueqlem  12697  smumullem  12699  gcdaddm  12724  bezoutlem1  12733  bezout  12737  gcddiv  12744  seq1st  12757  alginv  12761  algfx  12766  isprm2lem  12781  nn0gcdsq  12839  crt  12862  eulerthlem2  12866  pythagtriplem1  12885  iserodd  12904  pcqmul  12922  pcexp  12928  pcneg  12942  pcmpt  12956  pcfac  12963  prmreclem2  12980  prmreclem3  12981  1arith  12990  vdwpc  13043  ramcl  13092  imasval  13430  ercpbllem  13466  xpscfv  13480  iscat  13590  iscatd  13591  catideu  13593  iscatd2  13599  catlid  13601  catrid  13602  catass  13604  proplem  13608  homfeq  13613  comfeq  13625  catpropd  13628  moni  13655  epii  13662  sectffval  13669  sectfval  13670  oppcsect  13692  sectmon  13696  isfunc  13754  funcid  13760  funcco  13761  funcpropd  13790  isfull  13800  fthsect  13815  fthmon  13817  natfval  13836  isnat  13837  nati  13845  fucsect  13862  natpropd  13866  setcmon  13935  setcepi  13936  setcsect  13937  evlfcl  14012  uncfcurf  14029  yoniso  14075  isacs5lem  14288  acsdrscl  14289  acsficl  14290  latdisdlem  14308  latdisd  14309  isdlat  14312  dlatmjdi  14313  isps  14327  ismnd  14385  mgmidmo  14386  mndlem1  14387  mgmlrid  14405  ismndd  14412  mndpropd  14414  imasmnd2  14425  ismhm  14433  mhmpropd  14437  mhmlin  14438  mhmeql  14457  gsumvalx  14467  gsumval2  14476  gsumccat  14480  gsumwmhm  14483  frmdgsum  14500  isgrp  14509  grppropd  14516  isgrpd2e  14520  isgrpid2  14534  grpidd2  14535  grpinvfval  14536  grpinvpropd  14559  grpsubrcan  14563  grplactcnv  14580  mulgnn0p1  14594  mulgneg2  14610  mulgnnass  14611  mulgnn0ass  14612  mulgass  14613  mhmmulg  14615  imasgrp2  14626  isghm  14699  ghmlin  14704  ghmeql  14721  isga  14761  gagrpid  14764  gaass  14767  galcan  14774  orbsta  14783  cayleylem2  14804  cntzfval  14812  elcntz  14814  cntzsnval  14816  elcntzsn  14817  cntzi  14821  resscntz  14823  cntzmhm  14830  gsumwrev  14855  odfval  14864  mndodcong  14873  odbezout  14887  odeq1  14889  submod  14896  gexval  14905  gexdvds  14911  ispgp  14919  sylow1lem1  14925  sylow2alem1  14944  sylow2alem2  14945  sylow2blem2  14948  efgmnvl  15039  efgredlemc  15070  efgredeu  15077  frgpuptinv  15096  frgpup1  15100  frgpup3lem  15102  iscmn  15112  cmnpropd  15114  iscmnd  15117  abladdsub4  15131  submcmn2  15151  divsabl  15173  iscyg  15182  cygabl  15193  gsum2d  15239  dmdprd  15252  dprdval  15254  dprdfcntz  15266  subgdmdprd  15285  dprd2da  15293  dpjrid  15313  pgpfac1lem3a  15327  ablfaclem3  15338  ablfac2  15340  isrng  15361  rngpropd  15388  mulgass2  15403  imasrng  15418  dvdsr  15444  dvreq1  15491  isdrng  15532  drngprop  15539  isdrngd  15553  drngpropd  15555  isabv  15600  abvmul  15610  issrng  15631  issrngd  15642  islmod  15647  lmodlema  15648  islmodd  15649  lmodprop2d  15703  islmhm  15800  lmhmlin  15808  islmhm2  15811  lmhmeql  15828  lmhmpropd  15842  islbs  15845  lbspropd  15868  divscrng  16008  islpir  16017  rrgval  16044  unitrrg  16050  isassa  16072  assalem  16073  isassad  16079  assapropd  16083  mvrf1  16186  mplmonmul  16224  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  coe1tm  16365  ply1sclf1  16380  cnfldmulg  16422  cnfldexp  16423  prmirredlem  16462  chrcong  16499  zndvds  16519  znf1o  16521  znunit  16533  cygznlem3  16539  frgpcyg  16543  isphl  16548  ipcj  16554  iporthcom  16555  ip2eq  16573  isphld  16574  phlpropd  16575  ocvfval  16582  iscss  16599  ishil  16634  isobs  16636  obsip  16637  obslbs  16646  isperf  16898  restperf  16930  cmpsub  17143  iscon  17155  2ndcsep  17201  elptr2  17285  ptbasin  17288  dfac14  17328  txcnp  17330  ptcnplem  17331  ptcnp  17332  cnmpt11  17373  cnmpt21  17381  cnmptcom  17388  kqfeq  17431  isr0  17444  pt1hmeo  17513  imasdsf1olem  17953  isxms  18009  xmspropd  18035  imasf1oxms  18051  stdbdmopn  18080  isngp3  18136  ngppropd  18169  isnlm  18202  nmvs  18203  xrsxmet  18331  cnheibor  18469  htpyi  18488  htpycc  18494  pi1xfr  18569  pi1coghm  18575  isclm  18578  lmhmclm  18600  clmmulg  18607  iscph  18622  tchcph  18683  cmetcaulem  18730  bcth3  18769  ovolunlem1a  18871  ovolicc2lem1  18892  ovolicc2lem4  18895  ovolicc2  18897  mblsplit  18907  volun  18918  volfiniun  18920  voliunlem1  18923  volsup  18929  ioorinv  18947  uniioombllem2  18954  vitalilem3  18981  mbfeqalem  19013  mbflim  19039  itgeqa  19184  itgconst  19189  itgfsum  19197  itgsplitioo  19208  dvnadd  19294  dvnres  19296  dvexp  19318  dvmptfsum  19338  mvth  19355  dvlip  19356  lhop1lem  19376  dvcvx  19383  evlslem1  19415  mpfrcl  19418  evlsval  19419  mdegle0  19479  ply1nzb  19524  mon1pval  19543  facth1  19566  ig1pval  19574  dgrmulc  19668  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  coecj  19675  vieta1lem2  19707  vieta1  19708  elqaalem3  19717  dvntaylp  19766  ulmss  19790  mtest  19797  sineq0  19905  efif1olem4  19923  cxpexp  20031  mulcxplem  20047  mulcxp  20048  cxpmul2  20052  cxpeq  20113  affineequiv2  20140  quad2  20151  dcubic  20158  leibpi  20254  o1cxp  20285  scvxcvx  20296  wilthlem1  20322  wilthlem2  20323  perfect  20486  dchrelbas2  20492  dchrinv  20516  dchrptlem2  20520  lgsne0  20588  lgsqrlem2  20597  lgsdchr  20603  lgseisenlem2  20605  lgsquad2lem2  20614  dchrisumlem1  20654  qabvexp  20791  ostthlem1  20792  ostthlem2  20793  ostth3  20803  isgrpo  20879  grpoass  20886  grpoidinvlem3  20889  grpoidinv  20891  grpoideu  20892  grpoidinv2  20901  grpoinvfval  20907  isgrp2d  20918  gxcom  20952  gxinv  20953  gxnn0add  20957  gxnn0mul  20960  isablo  20966  ablocom  20968  gxdi  20979  issubgoilem  20992  isass  20999  opidon  21005  exidu1  21009  cmpidelt  21012  elghomlem2  21045  ghomlin  21047  ghgrplem2  21050  ghgrp  21051  ghablo  21052  isrngo  21061  rngoid  21066  rngoideu  21067  rngodi  21068  rngodir  21069  rngoass  21070  iscom2  21095  vci  21120  vcid  21123  vcdi  21124  vcdir  21125  vcass  21126  isvclem  21149  isnvlem  21182  nvmeq0  21238  nvs  21244  imsmetlem  21275  islno  21347  lnolin  21348  ishmo  21405  isphg  21411  phpar2  21417  phpar  21418  ipdiri  21424  ipasslem1  21425  ipasslem5  21429  ipasslem11  21434  ipassi  21435  dipdir  21436  dipass  21439  ip2eqi  21451  htth  21514  hvsubsub4  21655  hvnegdi  21662  hvaddcan  21665  hvaddcan2  21666  hvsubcan  21669  hvsubcan2  21670  hvaddsub4  21673  hial2eq  21701  normlem9at  21716  normsq  21729  norm-iii  21735  normsub  21738  normpyth  21740  normpar  21750  polid  21754  ococ  22001  chj0  22092  chlejb1  22107  chdmm1  22120  chjass  22128  spanun  22140  spansn  22154  elspansn2  22162  cmbr  22179  cmbr3  22203  pjoml2  22206  pjoml3  22207  osum  22240  spansnj  22242  pjch1  22265  pjadji  22280  pjaddi  22281  pjinormi  22282  pjsubi  22283  pjmuli  22284  pjcjt2  22287  pjch  22289  pjopyth  22315  pjpyth  22320  hoaddcom  22370  hoaddass  22378  hocsubdir  22381  hoaddid1  22387  ho0sub  22393  honegsub  22395  adjsym  22429  eigrei  22430  eigre  22431  eigposi  22432  eigorth  22434  ellnop  22454  elhmop  22469  ellnfn  22479  cnvadj  22488  lnopl  22510  unop  22511  hmop  22518  lnfnl  22527  adj1  22529  eleigvec  22553  hoddi  22586  lnopeq0lem2  22602  lnopunilem1  22606  lnopunilem2  22607  lnopunii  22608  elunop2  22609  lnophmi  22614  lnfnmul  22644  cnlnadjlem5  22667  branmfn  22701  bra11  22704  hmopidmchi  22747  hmopidmch  22749  hmopidmpj  22750  pjss2coi  22760  pjssmi  22761  pjssge0i  22762  pjidmco  22777  dfpjop  22778  elpjrn  22786  isst  22809  ishst  22810  hstel2  22815  stj  22831  mdbr  22890  mdi  22891  mdbr3  22893  dmdbr  22895  dmdmd  22896  dmdi  22898  dmdbr3  22901  mddmd2  22905  mdsl1i  22917  chjatom  22953  bcm1n  23048  xmulcand  23120  iuninc  23174  fmptcof2  23244  cnre2csqlem  23309  mndpluscn  23314  xrsmulgzz  23322  esumpr2  23454  esumcvg  23469  ofcfeqd2  23477  ismeas  23545  isrnmeas  23546  measvun  23552  probun  23637  subfacp1lem3  23728  subfacp1lem4  23729  subfacp1lem5  23730  subfacp1lem6  23731  subfacval2  23733  erdszelem9  23745  sconpht  23775  ptpcon  23779  cvmliftmolem1  23827  cvmliftmolem2  23828  cvmliftlem10  23840  cvmlift2  23862  cvmliftphtlem  23863  iseupa  23896  eupaseg  23903  eupap1  23915  eupath2  23919  ghomgrpilem1  24007  relexpsucr  24041  relexpsucl  24043  relexpcnv  24044  relexpadd  24050  sqdivzi  24094  mulcan2g  24100  faclim  24126  cprodeq2w  24134  cprodeq2ii  24135  zprod  24160  fprod  24164  fprodf1o  24172  fprb  24200  rdgprc  24222  dfrdg2  24223  preddowncl  24267  poseq  24324  soseq  24325  wfr3g  24326  wfrlem1  24327  wfrlem12  24338  wfrlem14  24340  wfrlem15  24341  wfr2  24344  wfr2c  24345  tfr3ALT  24350  frr3g  24351  frrlem1  24352  frrlem11  24364  sltval2  24381  sltres  24389  nofulllem5  24431  fvsingle  24530  fullfunfv  24557  brcgr  24600  brbtwn2  24605  colinearalglem1  24606  colinearalg  24610  ax5seglem1  24628  ax5seglem2  24629  ax5seglem8  24636  ax5seglem9  24637  axlowdimlem13  24654  axlowdimlem16  24657  axlowdim1  24659  axcontlem1  24664  axcontlem2  24665  axcontlem6  24669  axcontlem7  24670  axcontlem8  24671  lineelsb2  24843  bpolyval  24856  bpolydif  24862  rankung  24868  ranksng  24869  rankpwg  24871  surjsec2  25223  repfuntw  25263  islatalg  25286  labss1  25292  labss2  25294  prodeq3ii  25411  iscom  25436  iscomb  25437  ridlideq  25438  smgrpass2  25444  fprodadd  25455  mndoass2  25463  fprodneg  25481  fprodsub  25482  trooo  25497  rltrooo  25518  com2i  25519  vecval1b  25554  vecval3b  25555  vecax5b  25562  glmrngo  25585  vecax5c  25586  vri  25595  cnegvex2  25763  rnegvex2  25764  cnegvex2b  25765  rnegvex2b  25766  addcanri  25769  addcanrg  25770  isded  25839  dedi  25840  1ded  25841  idosd  25847  domcmpd  25849  codcmpd  25850  iscatOLD  25857  cati  25858  1cat  25862  cmpasso  25876  cmpida  25877  cmpidb  25878  ismona  25912  ismonb  25913  idmon  25920  isepia  25922  isepib  25923  isiso  25928  cinvlem1  25931  cinvlem2  25932  isfuna  25937  isfunb  25938  issrc  25970  propsrc  25971  isntr  25976  cmp2morp  26061  rocatval  26062  cmppar3  26077  selsubf3g  26095  pgapspf2  26156  xsyysx  26248  opnregcld  26351  cldregopn  26352  neibastop3  26414  cocanfo  26477  upixp  26506  sdclem2  26555  caushft  26580  ismtycnv  26629  ismtyima  26630  ismtybndlem  26633  ismtyres  26635  bfplem2  26650  bfp  26651  grpoeqdivid  26674  ghomco  26676  rngohomval  26698  isrngohom  26699  rngohomadd  26703  rngohommul  26704  iscringd  26727  crngocom  26729  crngohomfo  26734  dmncan2  26805  fnelfp  26858  ismrcd2  26877  ismrc  26879  dvdsrabdioph  26994  fphpdo  27003  rmxypairf1o  27099  monotoddzzfi  27130  monotoddzz  27131  oddcomabszz  27132  rmxdioph  27212  expdiophlem2  27218  dnnumch3  27247  aomclem8  27262  islssfg  27271  unxpwdom3  27359  gicabl  27366  pmtrfrn  27503  cntzsdrg  27613  idomodle  27615  fgraphxp  27633  hausgraph  27634  caofcan  27643  expgrowth  27655  fmuldfeq  27816  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  stoweidlem30  27882  stoweidlem48  27900  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  sbcfun  28090  csbafv12g  28105  csbaovg  28148  wlkntrllem4  28348  redwlk  28364  wlkdvspthlem  28365  iscrct  28369  iscycl  28370  fargshiftf1  28382  fargshiftfva  28384  eupatrl  28385  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3trllem5  28400  4cycl4v4e  28412  4cycl4dv4e  28414  bnj1385  29181  bnj66  29208  bnj106  29216  bnj155  29227  bnj222  29231  bnj540  29240  bnj591  29259  bnj594  29260  bnj611  29266  bnj893  29276  bnj1000  29289  bnj966  29292  bnj1112  29329  bnj1234  29359  bnj1253  29363  bnj1280  29366  bnj1326  29372  bnj1450  29396  bnj1463  29401  bnj1529  29416  lshpset  29790  lcvexchlem4  29849  lcvexchlem5  29850  lflset  29871  islfl  29872  lfli  29873  islfld  29874  eqlkr3  29913  isopos  29992  oposlem  29995  opcon3b  30008  cmtvalN  30023  omllaw  30055  cvlexchb2  30143  cvlatexchb2  30147  cvlsupr2  30155  4atlem9  30414  4atlem10a  30415  4atlem11a  30418  4atlem12a  30421  4at2  30425  pmapglb2N  30582  pmapglb2xN  30583  paddasslem17  30647  ispsubclN  30748  ispsubcl2N  30758  lhpmod2i2  30849  lhpmod6i1  30850  4atexlemex2  30882  4atex  30887  4atex2-0aOLDN  30889  4atex2-0cOLDN  30891  ldilval  30924  ltrnfset  30928  ltrnset  30929  isltrn  30930  ltrneq2  30959  trnfsetN  30966  trnsetN  30967  istrnN  30968  cdlemd5  31013  cdleme0moN  31036  cdleme0nex  31101  cdleme18d  31106  cdleme31so  31190  cdleme31fv  31201  cdlemg2jlemOLDN  31404  cdlemg2fvlem  31405  cdlemg2klem  31406  istendo  31571  tendovalco  31576  tendoeq2  31585  dicelvalN  31990  dihval  32044  dihcnv11  32087  dihmeetlem13N  32131  dihlspsnat  32145  dochn0nv  32187  dochkrshp4  32201  lpolsetN  32294  lpolsatN  32300  lpolpolsatN  32301  lcfl1lem  32303  lclkrlem2a  32319  lclkrlem2e  32323  lcfls1lem  32346  lclkrs2  32352  lcdfval  32400  lcdval  32401  mapdffval  32438  mapdfval  32439  mapd0  32477  mapdpglem30  32514  mapdhval  32536  mapdheq2  32541  hdmap1vallem  32610  hdmap1val  32611  hdmap1cbv  32615  hdmapval3N  32653  hdmap10  32655  hdmapeq0  32659  hdmap14lem12  32694  hdmap14lem13  32695  hgmapfval  32701  hgmapvs  32706  hgmapvv  32741  hlhilocv  32772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator