Theorem eqeq12d 1526

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

Syntax hints:   -> wi 3   <-> wb 144   = wceq 988

This theorem is referenced by:  eqeqan12d 1527  hbeqd 1951  uniprg 2564  unisng 2566  ordunisuc 3144  onsucuni2 3146  orduninsuc 3169  fveqres 3825  eqfnfvf 3874  fvreseq 3875  fnressn 3913  fvi 3918  tfrlem1 3987  tfrlem2 3988  tfrlem3 3989  tfrlem9 3995  tfrlem11 3997  tfrlem12 3998  tfr2 4001  tfr3 4002  tz7.44-1 4004  tz7.44-2 4005  tz7.44-3 4006  rdglem1 4013  rdg0g 4020  rdgsuc 4021  rdglim 4024  abianfp 4038  eqfnoprval 4093  caoprcom 4131  caoprass 4132  caoprcan 4133  caoprdistr 4137  caoprmo 4148  op1stg 4165  op2ndg 4166  oalim 4251  omlim 4252  oelim 4253  oa0r 4257  om0r 4258  om1r 4261  oaass 4279  oarec 4280  odi 4294  omass 4295  oelim2 4306  nnacom 4317  nnmsucr 4324  nnmcom 4325  oaabs 4336  ecoprcom 4406  ecoprass 4407  ecoprdi 4408  dom2d 4491  rankvalg 4755  ranklim 4771  rankonid 4781  rankr1id 4783  rankuni 4784  carduni 4947  cardprc 4950  alephcard 4956  alephfp2 4990  alephval3 4992  cardcf 5000  mulcanpi 5116  mulidpq 5158  genpv 5191  0idsr 5295  1idsr 5296  supsrlem2 5315  ax0id 5370  ax1id 5371  cnegexlem1 5434  cnegexlem3 5436  addcani 5440  addcan 5441  addcan2 5442  negsub 5471  negneg 5482  subid1 5485  subcan2 5491  subcan 5501  mulneg1 5540  mul2neg 5543  negdi 5544  mulcani 5775  mulcant2i 5776  mulcan 5777  mulcan2 5778  mulcan2OLD 5779  divcan1 5809  divreczi 5821  divrec 5822  divdirzi 5834  divdir 5835  divdirOLD 5836  divcan3 5841  div11 5844  div1 5852  recrec 5856  conjmul 5881  eqneg 5889  2times 6092  modadd1 6414  icoun 6473  snunioo 6475  om2uzsuci 6588  seq1lem1 6602  seq1res 6620  ser1add2i 6631  ser1addi 6632  seq1shftid 6649  seqzfveq 6677  expp1 6697  mulexp 6717  recexpOLD 6718  expadd 6719  expmul 6720  binom2 6772  sq01 6773  sqrthi 6822  sqrmuli 6828  sqrsq 6845  sqsqr 6846  cjreb 6923  cjmulval 6925  reneg 6927  readd 6928  imneg 6930  imadd 6931  cjcj 6934  cjadd 6935  cjmul 6936  cjneg 6937  addcj 6938  cjexp 6940  absval2 6975  absmul 6981  absdiv 6983  absid 6985  absexp 6991  cjdiv 7012  abssub 7017  recan 7028  abslem2 7032  caurei 7050  cauimi 7051  ser1absdiflem 7052  bcpasc2 7091  bcpasc 7093  fsum1slem 7131  fsump1slem 7135  fsum1ps 7141  fsumadd 7145  csbfsumlem 7149  csbfsum 7150  fsumcom 7151  fsumrev 7152  fsummulc1 7156  fsumconst 7161  serzmulci 7181  serzrelem 7184  binomlem6 7194  bcxmas 7199  climshft2i 7229  iserzshft2i 7230  climaddlem1 7237  climmullem6 7248  ser1consti 7294  cvgcmp2lem 7303  isumnn0nnai 7331  geoseri 7357  fsum0diag 7381  fsum0diag4 7384  efcj 7460  efadd 7490  efexp 7495  ef4p 7524  sinadd 7577  cosadd 7578  demoivre 7609  iscaunns 8064  isgrp 8161  grpass 8167  grpidinvlem3 8170  grpidinv 8172  grpideu 8173  grpidinv2 8179  grpinvfval 8185  isgrp2i 8195  isabl 8220  ablcom 8222  issubgilem 8240  cnid 8246  ghgrpilem1 8252  ghgrpilem4 8255  ghgrpi 8256  isring 8260  ringi 8261  ringid 8264  ringdi 8265  ringdir 8266  ringass 8267  ringsn 8282  vci 8286  vcid 8289  vcdi 8290  vcdir 8291  vcass 8292  isvclem 8315  isnvlem 8348  nvi 8352  nvmeq0 8403  nvs 8409  imsmetlem 8442  islno 8533  lnolin 8534  isphg 8595  phpar2 8601  phpar 8602  ipdiri 8608  ipasslem1 8609  ipasslem5 8613  ipasslem11 8619  ipassi 8620  ipdir 8621  ipass 8624  ip2eqi 8636  minveclem6 8669  minveclem7 8670  minveclem8 8671  htthlem2 8740  isps 8764  hvsubsub4 9046  hvnegdi 9053  hvaddcan 9056  hvaddcan2 9057  hvsubcan 9061  hvsubcan2 9062  hvaddsub4 9065  hial2eq 9092  normlem9at 9107  normsq 9121  norm-iii 9127  normsub 9130  normpyth 9132  normpar 9142  polid 9146  chocunii 9292  pjthlem8 9346  ococ 9368  axpjpj 9376  chj0 9540  chlejb1 9555  chdmm1 9568  chjass 9576  spanun 9588  spansn 9602  elspansn2 9610  cmbr 9647  cmbr3 9671  pjoml2 9674  pjoml3 9675  osum 9708  spansnj 9712  pjch1 9735  pjadji 9750  pjaddi 9751  pjinormi 9752  pjsubi 9753  pjmuli 9754  pjcjt2 9757  pjch 9759  pjopyth 9785  pjpyth 9790  hoaddcom 9820  hoaddass 9828  hocsubdir 9831  hoaddid1 9837  ho0sub 9843  honegsub 9845  adjsym 9879  eigrei 9880  eigre 9881  eigposi 9882  ellnop 9902  elhmop 9918  ellnfn 9928  cnvadj 9934  hhlnoi 9944  lnopl 9956  unop 9957  hmop 9964  lnfnl 9973  adj1 9975  eleigvec 9999  hoddi 10032  lnopeq0lem2 10048  lnopunilem1 10052  lnopunilem2 10053  lnopunii 10054  elunop2 10055  lnophmi 10060  lnfnmul 10094  cnlnadjlem5 10121  branmfn 10155  hmopidmchi 10196  hmopidmpji 10197  hmopidmch 10198  hmopidmpj 10199  pjss2coi 10209  pjssmi 10210  pjssge0i 10211  pjidmco 10226  pjhmopidm 10227  dfpjop 10228  stel 10259  hstel 10260  hstel2 10264  stj 10280  mdbr 10339  mdi 10340  mdbr3 10342  dmdbr 10344  dmdmd 10345  dmdi 10347  dmdbr3 10350  mddmd2 10354  mdsl1i 10366  chjatom 10402  elghomlem2 10504  ghomgrpilem1 10506  ghomlin 10514  cayleylem2 10531  erdisj2 10565  moec 10579  intprd 10589  vri 10625  limfillem2OLD 10732  iscon 10751  iscon2 10752  isded 10804  dedi 10805  1ded 10806  idosd 10812  domcmpd 10814  codcmpd 10815  iscat 10822  cati 10823  1cat 10827  cmpasso 10841  cmpida 10842  cmpidb 10843  ismona 10872  ismonb 10873  idmon 10880  isepia 10882  isepib 10883  cinvlem1 10890  cinvlem2 10891  isfuna 10896  isfunb 10897

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain