Theorem eqeq12d 1481

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 1475	. 2 |- (ph -> (A = C <-> B = C))
3		eqeq12d.2	. . 3 |- (ph -> C = D)
4	3	eqeq2d 1478	. 2 |- (ph -> (B = C <-> B = D))
5	2, 4	bitrd 526	1 |- (ph -> (A = C <-> B = D))

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

This theorem is referenced by:  eqeqan12d 1482  hbeqd 1904  uniprg 2506  unisng 2508  ordunisuc 3079  onsucuni2 3081  orduninsuc 3104  fveqres 3734  eqfnfvf 3783  fvreseq 3784  fnressn 3822  fvi 3827  tfrlem1 3896  tfrlem2 3897  tfrlem3 3898  tfrlem9 3904  tfrlem11 3906  tfrlem12 3907  tfr2 3910  tfr3 3911  tz7.44-1 3913  tz7.44-2 3914  tz7.44-3 3915  rdglem1 3922  rdg0t 3929  rdgsuct 3930  rdglimt 3933  abianfp 3947  eqfnoprval 4001  caoprcom 4039  caoprass 4040  caoprcan 4041  caoprdistr 4045  caoprmo 4056  op1stg 4071  op2ndg 4072  1st2val 4079  2nd2val 4080  df1st2 4110  df2nd2 4111  oalim 4151  omlim 4152  oelim 4153  oa0r 4157  om0r 4158  om1r 4161  oaass 4179  oarec 4180  odi 4194  omass 4195  oelim2 4206  nnacom 4217  nnmsucr 4224  nnmcom 4225  oaabs 4236  ecoprcom 4303  ecoprass 4304  ecoprdi 4305  dom2d 4385  rankvalg 4641  ranklim 4657  rankonid 4667  rankr1id 4669  rankuni 4670  carduni 4830  cardprc 4833  alephcard 4839  alephfp2 4873  alephval3 4875  cardcf 4883  mulcanpi 4999  mulidpq 5041  genpv 5074  0idsr 5178  1idsr 5179  supsrlem2 5198  ax0id 5253  ax1id 5254  cnegextlem1 5317  cnegextlem3 5319  addcan 5323  addcant 5324  addcan2t 5325  negsubt 5354  negnegt 5365  subid1t 5368  subcan2t 5374  subcant 5384  mulneg1t 5423  mul2negt 5426  negdit 5427  mulcan 5659  mulcant2 5660  mulcant 5661  mulcan2t 5662  divcan1t 5689  divcan2t 5690  divrecz 5701  divrect 5702  divdirz 5712  divdirt 5713  divcan3t 5718  div11t 5721  div1t 5729  recrect 5732  conjmult 5753  eqnegt 5761  2timest 5951  om2uzsuc 6233  seq1lem1 6246  seq1res 6264  ser1add2 6275  ser1add 6276  seq1shftid 6293  icoun 6346  snunioo 6348  seqzfveq 6486  expp1t 6506  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  binom2t 6581  sq01t 6582  sqrth 6629  sqrmul 6635  sqrsqt 6652  sqsqrt 6653  cjrebt 6735  cjmulvalt 6737  renegt 6739  readdt 6740  imnegt 6742  imaddt 6743  cjcjt 6746  cjaddt 6747  cjmult 6748  cjnegt 6749  addcjt 6750  cjexpt 6752  absval2t 6787  absmult 6793  absdivt 6795  absidt 6797  absexpt 6803  cjdivt 6827  abssubt 6832  recant 6842  abslem2 6846  caure 6864  cauim 6865  ser1absdiflem 6866  bcpasc2t 6906  bcpasct 6908  fsum1slem 6946  fsump1slem 6950  fsum1ps 6956  fsumadd 6960  csbfsumlem 6964  csbfsum 6965  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumconst 6976  serzmulc 6996  serzrelem 6999  binomlem6 7009  bcxmas 7014  climshft2 7043  iserzshft2 7044  climaddlem1 7050  climmullem6 7061  ser1const 7107  cvgcmp2lem 7116  isumnn0nna 7143  geoser 7169  fsum0diag 7193  fsum0diag4 7196  efcjt 7279  efaddt 7309  efexpt 7314  ef4pt 7341  sinaddt 7395  cosaddt 7396  demoivre 7426  isgrp 7975  grpass 7981  grpidinvlem3 7984  grpidinv 7986  grpideu 7987  grpidinv2 7994  grpinvfval 8000  isgrp2i 8011  isabl 8037  ablcom 8039  issubgilem 8058  cnid 8064  ghgrpilem1 8070  ghgrpilem4 8073  ghgrpi 8074  isring 8078  ringi 8079  ringid 8082  ringdi 8083  ringdir 8084  ringass 8085  ringsn 8100  vci 8104  vcid 8107  vcdi 8108  vcdir 8109  vcass 8110  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvmeq0 8224  nvs 8229  imsmetlem 8261  islno 8348  lnolin 8349  isphg 8407  phpar2 8413  phpar 8414  ipdiri 8420  ipasslem1 8421  ipasslem5 8425  ipasslem11 8431  ipassi 8432  ipdir 8433  ipass 8436  ip2eqi 8448  minveclem6 8481  minveclem7 8482  minveclem8 8483  htthlem2 8551  isps 8571  hvsubsub4t 8848  hvnegdit 8855  hvaddcant 8858  hvaddcan2t 8859  hvsubcant 8862  hvsubcan2t 8863  hvaddsub4t 8866  hial2eqt 8893  normlem9at 8908  normsqt 8922  norm-iiit 8928  normsubt 8931  normpytht 8933  normpart 8943  polidt 8947  chocuni 9088  pjthlem8 9141  ococt 9163  axpjpjt 9171  chj0t 9335  chlejb1t 9350  chdmm1t 9363  chjasst 9371  spanunt 9383  spansnt 9398  elspansn2t 9406  cmbrt 9444  cmbr3t 9468  pjoml2t 9471  pjoml3t 9472  osumt 9505  spansnjt 9509  pjch1t 9532  pjadjt 9547  pjaddt 9548  pjinormt 9549  pjsubt 9550  pjmult 9551  pjcjt2 9554  pjcht 9556  pjopytht 9582  pjpytht 9587  hoaddcomt 9617  hoaddasst 9625  hocsubdirt 9628  hoaddid1t 9634  ho0subt 9640  honegsubt 9642  adjsymt 9676  eigre 9677  eigret 9678  eigpos 9679  eigortht 9681  ellnopt 9701  elhmopt 9717  ellnfnt 9727  cnvadj 9733  hhlno 9743  lnoplt 9754  unopt 9755  hmopt 9762  lnfnlt 9771  adjt 9773  eleigvect 9797  hoddit 9830  lnopeq0lem2 9846  lnopunilem1 9850  lnopunilem2 9851  lnopuni 9852  elunop2t 9853  lnophm 9858  lnfnmult 9892  cnlnadjlem5 9919  branmfnt 9951  hmopidmch 9990  hmopidmpj 9991  hmopidmcht 9992  hmopidmpjt 9993  pjss2co 10003  pjssmt 10004  pjssge0t 10005  pjidmcot 10019  pjhmopidm 10020  dfpjopt 10021  stelt 10051  hstelt 10052  hstel2t 10056  stjt 10072  mdbrt 10131  mdit 10132  mdbr3 10134  dmdbrt 10136  dmdmdt 10137  dmdit 10139  dmdbr3 10141  mddmd 10144  mdsl1 10156  chjatom 10192  elghomlem2 10288  ghomgrpilem1 10290  ghomlin 10298  cayleylem2 10317  erdisj2 10343  moec 10357  intprd 10367  isded 10513  dedi 10514  1ded 10515  idosd 10521  domcmpd 10523  codcmpd 10524  iscat 10531  cati 10532  1cat 10536  cmpasso 10550  cmpida 10551  cmpidb 10552  ismona 10579  ismonb 10580  idmon 10588  isfuna 10592  isfunb 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain