Theorem eqeq12d 1488

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

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

This theorem is referenced by:  eqeqan12d 1489  hbeqd 1911  uniprg 2513  unisng 2515  ordunisuc 3086  onsucuni2 3088  orduninsuc 3111  fveqres 3746  eqfnfvf 3795  fvreseq 3796  fnressn 3834  fvi 3839  tfrlem1 3908  tfrlem2 3909  tfrlem3 3910  tfrlem9 3916  tfrlem11 3918  tfrlem12 3919  tfr2 3922  tfr3 3923  tz7.44-1 3925  tz7.44-2 3926  tz7.44-3 3927  rdglem1 3934  rdg0t 3941  rdgsuct 3942  rdglimt 3945  abianfp 3959  eqfnoprval 4013  caoprcom 4050  caoprass 4051  caoprcan 4052  caoprdistr 4056  caoprmo 4067  op1stg 4084  op2ndg 4085  1st2val 4092  2nd2val 4093  df1st2 4123  df2nd2 4124  oalim 4164  omlim 4165  oelim 4166  oa0r 4170  om0r 4171  om1r 4174  oaass 4192  oarec 4193  odi 4207  omass 4208  oelim2 4219  nnacom 4230  nnmsucr 4237  nnmcom 4238  oaabs 4249  ecoprcom 4316  ecoprass 4317  ecoprdi 4318  dom2d 4398  rankvalg 4656  ranklim 4672  rankonid 4682  rankr1id 4684  rankuni 4685  carduni 4845  cardprc 4848  alephcard 4854  alephfp2 4888  alephval3 4890  cardcf 4898  mulcanpi 5014  mulidpq 5056  genpv 5089  0idsr 5193  1idsr 5194  supsrlem2 5213  ax0id 5268  ax1id 5269  cnegextlem1 5332  cnegextlem3 5334  addcan 5338  addcant 5339  addcan2t 5340  negsubt 5369  negnegt 5380  subid1t 5383  subcan2t 5389  subcant 5399  mulneg1t 5438  mul2negt 5441  negdit 5442  mulcan 5673  mulcant2 5674  mulcant 5675  mulcan2t 5676  divcan1t 5703  divcan2t 5704  divrecz 5715  divrect 5716  divdirz 5726  divdirt 5727  divcan3t 5732  div11t 5735  div1t 5743  recrect 5746  conjmult 5767  eqnegt 5775  2timest 5965  om2uzsuc 6251  seq1lem1 6264  seq1res 6282  ser1add2 6293  ser1add 6294  seq1shftid 6311  icoun 6364  snunioo 6366  seqzfveq 6504  expp1t 6524  mulexpt 6544  recexpt 6545  expaddt 6546  expmult 6547  binom2t 6600  sq01t 6601  sqrth 6650  sqrmul 6656  sqrsqt 6673  sqsqrt 6674  cjrebt 6761  cjmulvalt 6763  renegt 6765  readdt 6766  imnegt 6768  imaddt 6769  cjcjt 6772  cjaddt 6773  cjmult 6774  cjnegt 6775  addcjt 6776  cjexpt 6778  absval2t 6814  absmult 6820  absdivt 6822  absidt 6824  absexpt 6830  cjdivt 6854  abssubt 6859  recant 6870  recantOLD 6871  abslem2 6875  caure 6893  cauim 6894  ser1absdiflem 6895  bcpasc2t 6936  bcpasct 6938  fsum1slem 6976  fsump1slem 6980  fsum1ps 6986  fsumadd 6990  csbfsumlem 6994  csbfsum 6995  fsumcom 6996  fsumrev 6997  fsummulc1 7001  fsumconst 7006  serzmulc 7026  serzrelem 7029  binomlem6 7039  bcxmas 7044  climshft2 7074  iserzshft2 7075  climaddlem1 7083  climmullem6 7094  ser1const 7142  cvgcmp2lem 7151  isumnn0nna 7179  geoser 7205  fsum0diag 7229  fsum0diag4 7232  efcjt 7315  efaddt 7345  efexpt 7350  ef4pt 7377  sinaddt 7431  cosaddt 7432  demoivre 7462  iscaunns 7927  isgrp 8024  grpass 8030  grpidinvlem3 8033  grpidinv 8035  grpideu 8036  grpidinv2 8043  grpinvfval 8049  isgrp2i 8059  isabl 8085  ablcom 8087  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 8309  islno 8400  lnolin 8401  isphg 8460  phpar2 8466  phpar 8467  ipdiri 8473  ipasslem1 8474  ipasslem5 8478  ipasslem11 8484  ipassi 8485  ipdir 8486  ipass 8489  ip2eqi 8501  minveclem6 8534  minveclem7 8535  minveclem8 8536  htthlem2 8604  isps 8628  hvsubsub4t 8911  hvnegdit 8918  hvaddcant 8921  hvaddcan2t 8922  hvsubcant 8925  hvsubcan2t 8926  hvaddsub4t 8929  hial2eqt 8956  normlem9at 8971  normsqt 8985  norm-iiit 8991  normsubt 8994  normpytht 8996  normpart 9006  polidt 9010  chocuni 9160  pjthlem8 9214  ococt 9236  axpjpjt 9244  chj0t 9408  chlejb1t 9423  chdmm1t 9436  chjasst 9444  spanunt 9456  spansnt 9471  elspansn2t 9479  cmbrt 9517  cmbr3t 9541  pjoml2t 9544  pjoml3t 9545  osumt 9578  spansnjt 9582  pjch1t 9606  pjadjt 9621  pjaddt 9622  pjinormt 9623  pjsubt 9624  pjmult 9625  pjcjt2 9628  pjcht 9630  pjopytht 9656  pjpytht 9661  hoaddcomt 9691  hoaddasst 9699  hocsubdirt 9702  hoaddid1t 9708  ho0subt 9714  honegsubt 9716  adjsymt 9750  eigre 9751  eigret 9752  eigpos 9753  eigortht 9755  ellnopt 9775  elhmopt 9791  ellnfnt 9801  cnvadj 9807  hhlno 9817  lnoplt 9829  unopt 9830  hmopt 9837  lnfnlt 9846  adjt 9848  eleigvect 9872  hoddit 9906  lnopeq0lem2 9922  lnopunilem1 9926  lnopunilem2 9927  lnopuni 9928  elunop2t 9929  lnophm 9934  lnfnmult 9968  cnlnadjlem5 9995  branmfnt 10029  hmopidmch 10070  hmopidmpj 10071  hmopidmcht 10072  hmopidmpjt 10073  pjss2co 10083  pjssmt 10084  pjssge0t 10085  pjidmcot 10100  pjhmopidm 10101  dfpjopt 10102  stelt 10132  hstelt 10133  hstel2t 10137  stjt 10153  mdbrt 10212  mdit 10213  mdbr3 10215  dmdbrt 10217  dmdmdt 10218  dmdit 10220  dmdbr3 10223  mddmd 10227  mdsl1 10239  chjatom 10275  elghomlem2 10374  ghomgrpilem1 10376  ghomlin 10384  cayleylem2 10401  erdisj2 10436  moec 10450  intprd 10460  limfillem2 10559  isded 10620  dedi 10621  1ded 10622  idosd 10628  domcmpd 10630  codcmpd 10631  iscat 10638  cati 10639  1cat 10643  cmpasso 10657  cmpida 10658  cmpidb 10659  ismona 10686  ismonb 10687  idmon 10695  isfuna 10699  isfunb 10700

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

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

Copyright terms: Public domain