Theorem eqeq12d 1489

Description: A useful inference for substituting definitions into an equality.

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	. . 3 |- (ph -> A = B)
2	1	eqeq1d 1483	. 2 |- (ph -> (A = C <-> B = C))
3		eqeq12d.2	. . 3 |- (ph -> C = D)
4	3	eqeq2d 1486	. 2 |- (ph -> (B = C <-> B = D))
5	2, 4	bitrd 528	1 |- (ph -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956

This theorem is referenced by:  eqeqan12d 1490  hbeqd 1913  uniprg 2516  unisng 2518  ordunisuc 3089  onsucuni2 3091  orduninsuc 3114  fveqres 3749  eqfnfvf 3798  fvreseq 3799  fnressn 3837  fvi 3842  tfrlem1 3911  tfrlem2 3912  tfrlem3 3913  tfrlem9 3919  tfrlem11 3921  tfrlem12 3922  tfr2 3925  tfr3 3926  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  rdglem1 3937  rdg0t 3944  rdgsuct 3945  rdglimt 3948  abianfp 3962  eqfnoprval 4016  caoprcom 4053  caoprass 4054  caoprcan 4055  caoprdistr 4059  caoprmo 4070  op1stg 4087  op2ndg 4088  1st2val 4095  2nd2val 4096  df1st2 4126  df2nd2 4127  oalim 4167  omlim 4168  oelim 4169  oa0r 4173  om0r 4174  om1r 4177  oaass 4195  oarec 4196  odi 4210  omass 4211  oelim2 4222  nnacom 4233  nnmsucr 4240  nnmcom 4241  oaabs 4252  ecoprcom 4319  ecoprass 4320  ecoprdi 4321  dom2d 4403  rankvalg 4661  ranklim 4677  rankonid 4687  rankr1id 4689  rankuni 4690  carduni 4850  cardprc 4853  alephcard 4859  alephfp2 4893  alephval3 4895  cardcf 4903  mulcanpi 5019  mulidpq 5061  genpv 5094  0idsr 5198  1idsr 5199  supsrlem2 5218  ax0id 5273  ax1id 5274  cnegextlem1 5337  cnegextlem3 5339  addcan 5343  addcant 5344  addcan2t 5345  negsubt 5374  negnegt 5385  subid1t 5388  subcan2t 5394  subcant 5404  mulneg1t 5443  mul2negt 5446  negdit 5447  mulcan 5677  mulcanOLD 5678  mulcant2OLD 5679  mulcantOLD 5680  mulcan2tOLD 5681  divcan1t 5712  divcan1tOLD 5713  divcan2tOLD 5715  divrecz 5726  divrect 5727  divdirz 5737  divdirt 5738  divdirtOLD 5739  divcan3t 5748  divcan3tOLD 5749  div11t 5753  div1t 5761  recrect 5764  conjmult 5785  eqnegt 5793  2timest 5992  om2uzsuc 6282  seq1lem1 6295  seq1res 6313  ser1add2 6324  ser1add 6325  seq1shftid 6342  icoun 6399  snunioo 6401  seqzfveq 6540  expp1t 6560  mulexpt 6580  recexpt 6581  expaddt 6582  expmult 6583  binom2t 6636  sq01t 6637  sqrth 6685  sqrmul 6691  sqrsqt 6708  sqsqrt 6709  cjrebt 6785  cjmulvalt 6787  renegt 6789  readdt 6790  imnegt 6792  imaddt 6793  cjcjt 6796  cjaddt 6797  cjmult 6798  cjnegt 6799  addcjt 6800  cjexpt 6802  absval2t 6837  absmult 6843  absdivt 6845  absidt 6847  absexpt 6853  cjdivt 6874  abssubt 6879  recant 6890  abslem2 6894  caure 6912  cauim 6913  ser1absdiflem 6914  bcpasc2t 6953  bcpasct 6955  fsum1slem 6993  fsump1slem 6997  fsum1ps 7003  fsumadd 7007  csbfsumlem 7011  csbfsum 7012  fsumcom 7013  fsumrev 7014  fsummulc1 7018  fsumconst 7023  serzmulc 7043  serzrelem 7046  binomlem6 7056  bcxmas 7061  climshft2 7091  iserzshft2 7092  climaddlem1 7099  climmullem6 7110  ser1const 7156  cvgcmp2lem 7165  isumnn0nna 7193  geoser 7219  fsum0diag 7243  fsum0diag4 7246  efcjt 7322  efaddt 7352  efexpt 7357  ef4pt 7385  sinaddt 7438  cosaddt 7439  demoivre 7469  iscaunns 7929  isgrp 8026  grpass 8032  grpidinvlem3 8035  grpidinv 8037  grpideu 8038  grpidinv2 8045  grpinvfval 8051  isgrp2i 8061  isabl 8086  ablcom 8088  issubgilem 8106  cnid 8112  ghgrpilem1 8118  ghgrpilem4 8121  ghgrpi 8122  isring 8126  ringi 8127  ringid 8130  ringdi 8131  ringdir 8132  ringass 8133  ringsn 8148  vci 8152  vcid 8155  vcdi 8156  vcdir 8157  vcass 8158  isvclem 8181  isnvlem 8214  nvi 8218  nvmeq0 8269  nvs 8275  imsmetlem 8308  islno 8399  lnolin 8400  isphg 8461  phpar2 8467  phpar 8468  ipdiri 8474  ipasslem1 8475  ipasslem5 8479  ipasslem11 8485  ipassi 8486  ipdir 8487  ipass 8490  ip2eqi 8502  minveclem6 8535  minveclem7 8536  minveclem8 8537  htthlem2 8606  isps 8630  hvsubsub4t 8912  hvnegdit 8919  hvaddcant 8922  hvaddcan2t 8923  hvsubcant 8926  hvsubcan2t 8927  hvaddsub4t 8930  hial2eqt 8957  normlem9at 8972  normsqt 8986  norm-iiit 8992  normsubt 8995  normpytht 8997  normpart 9007  polidt 9011  chocuni 9157  pjthlem8 9211  ococt 9233  axpjpjt 9241  chj0t 9405  chlejb1t 9420  chdmm1t 9433  chjasst 9441  spanunt 9453  spansnt 9467  elspansn2t 9475  cmbrt 9512  cmbr3t 9536  pjoml2t 9539  pjoml3t 9540  osumt 9573  spansnjt 9577  pjch1t 9600  pjadjt 9615  pjaddt 9616  pjinormt 9617  pjsubt 9618  pjmult 9619  pjcjt2 9622  pjcht 9624  pjopytht 9650  pjpytht 9655  hoaddcomt 9685  hoaddasst 9693  hocsubdirt 9696  hoaddid1t 9702  ho0subt 9708  honegsubt 9710  adjsymt 9744  eigre 9745  eigret 9746  eigpos 9747  eigortht 9749  ellnopt 9769  elhmopt 9785  ellnfnt 9795  cnvadj 9801  hhlno 9811  lnoplt 9823  unopt 9824  hmopt 9831  lnfnlt 9840  adjt 9842  eleigvect 9866  hoddit 9900  lnopeq0lem2 9916  lnopunilem1 9920  lnopunilem2 9921  lnopuni 9922  elunop2t 9923  lnophm 9928  lnfnmult 9962  cnlnadjlem5 9989  branmfnt 10023  hmopidmch 10064  hmopidmpj 10065  hmopidmcht 10066  hmopidmpjt 10067  pjss2co 10077  pjssmt 10078  pjssge0t 10079  pjidmcot 10094  pjhmopidm 10095  dfpjopt 10096  stelt 10126  hstelt 10127  hstel2t 10131  stjt 10147  mdbrt 10206  mdit 10207  mdbr3 10209  dmdbrt 10211  dmdmdt 10212  dmdit 10214  dmdbr3 10217  mddmd 10221  mdsl1 10233  chjatom 10269  elghomlem2 10368  ghomgrpilem1 10370  ghomlin 10378  cayleylem2 10395  erdisj2 10426  moec 10440  intprd 10450  limfillem2 10551  isded 10612  dedi 10613  1ded 10614  idosd 10620  domcmpd 10622  codcmpd 10623  iscat 10630  cati 10631  1cat 10635  cmpasso 10649  cmpida 10650  cmpidb 10651  ismona 10678  ismonb 10679  idmon 10687  isfuna 10691  isfunb 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain