Theorem eqeq12d 2155

Description: A useful inference for substituting definitions into an equality. (The proof was 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

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 |- (ph -> A = B)
2		eqeq12d.2	. 2 |- (ph -> C = D)
3		eqeq12 2153	. 2 |- ((A = B /\ C = D) -> (A = C <-> B = D))
4	1, 2, 3	syl11anc 659	1 |- (ph -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 219   = wceq 1586

This theorem is referenced by:  hbeqd 2665  hbeqdOLD 2666  sbceqg 2786  csbing 3013  csbifg 3198  uniprg 3381  unisng 3383  intprg 3432  limeq 3823  reusn 3956  ordunisuc 4053  onsucuni2 4055  orduninsuc 4064  csbfv12gALT 4775  fveqres 4793  fvsng 4845  eqfnfv2f 4856  fvreseq 4858  fnressn 4905  fvi 4910  csboprg 5006  eqfnoprv 5038  caoprcom 5079  caoprass 5080  caoprcan 5081  caoprdistr 5085  caoprmo 5096  op1stg 5134  op2ndg 5135  onfununi 5253  tfrlem1 5282  tfrlem2 5283  tfrlem3 5284  tfrlem3a 5285  tfrlem9 5291  tfrlem11 5293  tfrlem12 5294  tfr2 5297  tfr3 5298  tz7.44-1 5300  tz7.44-2 5301  tz7.44-3 5302  rdglem1 5309  rdg0g 5316  rdgsuc 5317  rdglim 5320  abianfp 5338  oalim 5378  omlim 5379  oelim 5380  oa0r 5384  om0r 5385  om1r 5388  oaass 5406  oarec 5407  odi 5421  omass 5422  oelim2 5436  oeoalem 5437  oeoa 5438  oeoelem 5439  oeoe 5440  nnacom 5451  nnmsucr 5458  nnmcom 5459  oaabs 5470  erdisj2 5505  ecoprcom 5539  ecoprass 5540  ecoprdi 5541  dom2d 5624  csbriotag 5742  unxpdomlem3 5819  ordiso 5914  rankvalg 6016  ranklim 6032  rankonid 6042  rankr1id 6044  rankuni 6045  cardprclem 6134  cardprc 6135  carduni 6136  alephcard 6156  alephfp2 6232  alephval3 6233  onacda 6259  cardcf 6271  axcc2lem 6293  axdc3lem2 6306  axdc4lem 6310  carduniOLD 6424  cardprcOLD 6426  alephcardOLD 6431  nnacdaOLD 6455  mulcanpi 6545  mulidpq 6587  genpv 6620  0idsr 6724  1idsr 6725  supsrlem2 6744  ax1rid 6798  mulid1 6832  readdcan 6969  mul02lem1 6971  addid1 6977  addcani 6983  addcan2i 6984  addcan 6985  addcan2 6986  addcom 6988  negsub 7035  negneg 7046  subid1 7049  subcan2 7055  subcan 7065  mulneg1 7088  negdi 7092  mulcani 7210  mulcant2i 7211  mulcan 7212  mulcan2 7213  divcan1 7240  divreczi 7252  divrec 7253  divdirzi 7263  divdir 7264  divcan3 7269  div11 7272  div1 7280  recrec 7283  conjmul 7306  eqneg 7314  2times 7521  modadd1 7864  modmul1 7865  icoun 7928  snunioo 7930  fzprval 8050  fztpval 8051  om2uzsuci 8078  cardfzOLD 8092  seq1lem1 8095  seq1res 8113  seq11g 8114  seq1p1g 8115  ser1add2i 8126  ser1addi 8127  seq1shftid 8144  seqz1g 8172  seqzp1g 8173  seq1seqzg 8174  seqzfveq 8175  seqzfveqg 8177  seq1resval2g 8188  expp1 8201  mulexp 8220  exprec 8221  exprecOLD 8222  expadd 8223  expmul 8224  binom2 8280  sq01 8281  sqrthi 8333  sqrmuli 8339  sqrsq 8356  sqsqr 8357  cjreb 8434  cjmulval 8436  reneg 8438  readd 8439  imneg 8441  imadd 8442  cjcj 8445  cjadd 8446  cjmul 8447  cjneg 8448  addcj 8449  cjexp 8451  absval2 8487  absmul 8493  absdiv 8495  absid 8497  absexp 8503  cjdiv 8525  abssub 8531  recan 8542  abslem2 8546  caurei 8564  cauimi 8565  ser1absdiflem 8566  bcpasc2 8605  bcpasc 8607  fsum1slem 8664  fsump1slem 8668  fsum1ps 8674  fsumadd 8678  csbfsumlem 8682  csbfsum 8683  fsumcom 8684  fsumrev 8685  fsummulc1 8689  fsumconst 8694  serzmulci 8714  serzrelem 8717  binomlem6 8727  bcxmas 8732  climshft2i 8762  iserzshft2i 8763  climaddlem1 8770  climmullem6 8781  ser1consti 8827  cvgcmp2lem 8836  isumnn0nnai 8865  geoseri 8894  fsum0diag 8918  fsum0diag4 8921  efcj 8997  efadd 9027  efexp 9032  ef4p 9063  sinadd 9116  cosadd 9117  demoivre 9150  gcdaddm 9329  alginv 9338  algfx 9343  eucalgval 9344  eucalginv 9347  eucalg 9350  mulgcdlem1 9351  mulgcdlem2 9352  mulgcdlem6 9356  isprm2lem 9368  1arithlem21 9414  1arithlem29 9423  strcval 9428  isgrp 9464  grplem1 9469  grpidinvlem3 9475  grpidinv 9477  grpideu 9478  grpidinv2 9484  grpinvfval 9490  isabl 9500  ablcom 9503  isring 9508  ringi 9509  ringideu 9512  ringidmlem 9518  istps 9717  iscaunns 10088  isgrpo 10187  grp2grpo 10190  grpoass 10196  grpoidinvlem3 10199  grpoidinv 10201  grpoideu 10202  grpoidval 10211  grpoidinv2 10213  grpoinvfval 10219  isgrp2i 10229  gxnn0suc 10256  gxcom 10261  gxinv 10262  gxnn0add 10266  gxnn0mul 10269  isablo 10278  ablocom 10280  gxdi 10291  issubgilem 10299  cnid 10304  addinv 10305  ghgrpilem1 10310  ghgrpilem4 10313  ghgrpi 10314  isgalem 10318  gagrpid 10327  gaass 10328  isringo 10334  ringoi 10335  ringid 10338  ringoideu 10339  ringodi 10340  ringodir 10341  ringoass 10342  ringsn 10359  vci 10368  vcid 10371  vcdi 10372  vcdir 10373  vcass 10374  isvclem 10397  isnvlem 10430  nvi 10434  nvmeq0 10485  nvs 10491  imsmetlem 10524  vacnlem1 10536  islno 10622  lnolin 10623  ishmo 10680  isphg 10686  phpar2 10692  phpar 10693  ipdiri 10699  ipasslem1 10700  ipasslem5 10704  ipasslem11 10710  ipassi 10711  ipdir 10712  ipass 10715  ip2eqi 10727  minveclem6 10764  minveclem7 10765  minveclem8 10766  htthlem2 10839  isps 10859  sineq0re 10938  elghomlem2 11026  ghomlin 11028  subsp 11080  fgf 11121  iscon 11177  iscon2 11178  isass 11201  opidon 11207  exidu1 11211  cmpidelt 11214  iscom2 11234  rngmgmbs4 11239  zrdivrng 11256  hvsubsub4 11397  hvnegdi 11404  hvaddcan 11407  hvaddcan2 11408  hvsubcan 11411  hvsubcan2 11412  hvaddsub4 11415  hial2eq 11442  normlem9at 11457  normsq 11470  norm-iii 11476  normsub 11479  normpyth 11481  normpar 11491  polid 11495  chocunii 11639  pjthlem8 11693  ococ 11715  axpjpj 11723  chj0 11887  chlejb1 11902  chdmm1 11915  chjass 11923  spanun 11935  spansn 11949  elspansn2 11957  cmbr 11992  cmbr3 12016  pjoml2 12019  pjoml3 12020  osum 12055  spansnj 12059  pjch1 12082  pjadji 12097  pjaddi 12098  pjinormi 12099  pjsubi 12100  pjmuli 12101  pjcjt2 12104  pjch 12106  pjopyth 12132  pjpyth 12137  hoaddcom 12169  hoaddass 12177  hocsubdir 12180  hoaddid1 12186  ho0sub 12192  honegsub 12194  adjsym 12228  eigrei 12229  eigre 12230  eigposi 12231  eigorth 12233  ellnop 12253  elhmop 12269  ellnfn 12279  cnvadj 12285  hhlnoi 12295  lnopl 12307  unop 12308  hmop 12315  lnfnl 12324  adj1 12326  eleigvec 12350  hoddi 12384  lnopeq0lem2 12400  lnopunilem1 12404  lnopunilem2 12405  lnopunii 12406  elunop2 12407  lnophmi 12412  lnfnmul 12446  cnlnadjlem5 12473  branmfn 12507  opsqrlem4 12545  hmopidmchi 12554  hmopidmpji 12555  hmopidmch 12556  hmopidmpj 12557  pjss2coi 12567  pjssmi 12568  pjssge0i 12569  pjidmco 12584  pjhmopidm 12585  dfpjop 12586  stel 12617  hstel 12618  hstel2 12622  stj 12638  mdbr 12697  mdi 12698  mdbr3 12700  dmdbr 12702  dmdmd 12703  dmdi 12705  dmdbr3 12708  mddmd2 12712  mdsl1i 12724  chjatom 12760  bnj1272 13799  bnj1385 13873  bnj64 13972  bnj106 13996  bnj155 14017  bnj222 14022  bnj540 14038  bnj589 14068  bnj591 14070  bnj594 14071  bnj611 14078  bnj892 14093  bnj965 14117  bnj966 14119  bnj1000 14135  bnj1112 14189  bnj1234 14231  bnj1253 14241  bnj1283 14247  bnj1280 14254  bnj1326 14267  bnj1450 14312  bnj1463 14321  bnj1529 14345  bnj1530 14346  hashgadd 14358  hashxplem 14361  hashxp 14362  hashpw 14364  ghomgrpilem1 14365  cayleylem2 14379  preddowncl 14550  poseq 14607  soseq 14608  wfr3g 14609  wfrlem1 14610  wfrlem12 14621  wfrlem14 14623  wfrlem15 14624  wfr2 14627  tfr3ALT 14632  frr3g 14633  frrlem1 14634  frrlem11 14646  sltval2 14662  sltres 14670  axfelem14 14712  axfelem18 14716  axfelem20 14718  axfelem22 14720  moec 15059  njtlc 15099  surrc2 15100  surjsec2 15179  cmpbvb 15211  repfuntw 15241  cbicplem 15247  iscst2 15259  iserzmulc1b 15267  islatalg 15270  labss1 15276  labss2 15278  fprod1slem 15415  fprodp1slem 15420  fprodp1s1 15422  iscom 15428  iscomb 15429  ridlideq 15430  smgrpass2 15436  fincmpzer 15446  fprodadd 15448  seqzp2 15451  mndass2 15456  curgrpact 15470  fprodneg 15476  fprodsub 15477  trooo 15492  cmprtr 15494  rltrooo 15517  com2i 15518  ununr 15522  vecval1b 15547  vecval3b 15548  vecax5b 15555  vecax5c 15578  vri 15587  subsp2OLD 15664  limfillem2 15705  clindistop2 15741  grphmlem2 15770  grphlem3 15771  isded 15877  dedi 15878  1ded 15879  idosd 15885  domcmpd 15887  codcmpd 15888  iscat 15895  cati 15896  1cat 15900  cmpasso 15914  cmpida 15915  cmpidb 15916  ismona 15952  ismonb 15953  idmon 15960  isepia 15962  isepib 15963  cinvlem1 15970  cinvlem2 15971  isfuna 15976  isfunb 15977  tarval2g 16060  isplibg0 16117  cbvcsb 16178  fictb 16195  ordisoOLD 16198  opnregcld 16239  cldregopn 16240  compsub 16255  topfneec 16325  comppfsc 16341  ist1-3 16367  fcluscf 16436  cocanfo 16513  upixp 16553  erthdmg 16554  seq11gOLD 16628  seq1p1gOLD 16629  seqz1gOLD 16630  seqzp1gOLD 16631  seq1seqzgOLD 16632  sdclem1 16633  sdc 16635  seq1eq2 16641  isumshft2 16654  mettrifi 16671  mettrifi2 16672  caushft 16675  oprpiece1res2 16705  isbnd 16763  ismtycnv 16773  ismtyhmeolem 16774  ismtyhmeo 16775  ismtybndlem 16776  ismtyres 16778  heiborlem11 16789  heiborlem32 16810  heiborlem35 16813  bfplem8 16829  bfplem10 16831  grpeqdivid 16862  ghomco 16864  phtpycom 16874  phtpycolem2 16876  phtpycolem3 16877  phtpycolem4 16878  phtpyco 16880  reparpht 16889  pcohtpylem2 16905  pcohtpy 16907  pi1gp 16919  isrnghom 16943  rnghomadd 16947  rnghommul 16948  iscringd 16971  crngcom 16973  crnghomfo 16978  dmncan2 17049  isopos 17576  oposlem 17579  opcon3b 17590  cmtval 17605  omllaw 17637  cvlexchb2 17728  cvlatexchb2 17732  cvlsupr2 17740  issrng 17888  islvec 17900  isphil 17907  ocvfval 17918  iscsubsp 17921  ishil 17922  4atlem9 18035  4atlem10a 18036  4atlem11a 18039  4atlem12a 18042  4at2 18046  pmapglb2 18203  pmapglb2x 18204  paddasslem17 18268  ispsubcl 18351  ispsubcl2 18361  lhpmod2i2 18434  ldilval 18467  ltrnfset 18470  ltrnset 18471  isltrn 18472  ltrnateq 18494  trnfset 18500  trnset 18501  istrn 18502  4atexlemex2 18541  cdlemd5 18570  cdleme0mo 18594  cdleme0nex 18661  cdleme18d 18666  cdleme31so 18752  cdleme31fv 18764  cdlemg2jlemOLD 18971  cdlemg2jlemOLDOLD 18972  cdlemg2fvlem 18973  cdlemg2klem 18974

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-17 1605  ax-4 1608  ax-5o 1610  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-an 339  df-cleq 2134

Copyright terms: Public domain