Theorem eqeq12d 1532

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

Hypotheses

Ref	Expression
eqeq12d.1	⊢ (φ → A = B)
eqeq12d.2	⊢ (φ → C = D)

Assertion

Ref	Expression
eqeq12d	⊢ (φ → (A = C ↔ B = D))

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. . 3 ⊢ (φ → A = B)
2	1	eqeq1d 1526	. 2 ⊢ (φ → (A = C ↔ B = C))
3		eqeq12d.2	. . 3 ⊢ (φ → C = D)
4	3	eqeq2d 1529	. 2 ⊢ (φ → (B = C ↔ B = D))
5	2, 4	bitrd 531	1 ⊢ (φ → (A = C ↔ B = D))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992

This theorem is referenced by:  eqeqan12d 1533  hbeqd 1959  uniprg 2582  unisng 2585  ordunisuc 3186  onsucuni2 3188  orduninsuc 3197  fveqres 3860  eqfnfvf2 3912  fvreseq 3913  fnressn 3951  fvi 3956  eqfnoprv 4076  caoprcom 4114  caoprass 4115  caoprcan 4116  caoprdistr 4120  caoprmo 4131  op1stg 4148  op2ndg 4149  onfununi 4209  tfrlem1 4212  tfrlem2 4213  tfrlem3 4214  tfrlem9 4220  tfrlem11 4222  tfrlem12 4223  tfr2 4226  tfr3 4227  tz7.44-1 4229  tz7.44-2 4230  tz7.44-3 4231  rdglem1 4238  rdg0g 4245  rdgsuc 4246  rdglim 4249  abianfp 4263  oalim 4303  omlim 4304  oelim 4305  oa0r 4309  om0r 4310  om1r 4313  oaass 4331  oarec 4332  odi 4346  omass 4347  oelim2 4358  oeoalem 4359  oeoa 4360  oeoelem 4361  oeoe 4362  nnacom 4373  nnmsucr 4380  nnmcom 4381  oaabs 4392  ecoprcom 4460  ecoprass 4461  ecoprdi 4462  dom2d 4545  rankvalg 4815  ranklim 4831  rankonid 4841  rankr1id 4843  rankuni 4844  carduni 5008  cardprc 5011  alephcard 5017  alephfp2 5051  alephval3 5053  cardcf 5061  nnacda 5090  mulcanpi 5181  mulidpq 5223  genpv 5256  0idsr 5360  1idsr 5361  supsrlem2 5380  ax0id 5435  ax1id 5436  cnegexlem1 5499  cnegexlem3 5501  addcani 5505  addcan 5506  addcan2 5507  negsub 5536  negneg 5547  subid1 5550  subcan2 5556  subcan 5566  mulneg1 5605  mul2neg 5608  negdi 5609  mulcani 5842  mulcant2i 5843  mulcan 5844  mulcan2 5845  divcan1 5872  divreczi 5884  divrec 5885  divdirzi 5895  divdir 5896  divcan3 5901  div11 5904  div1 5912  recrec 5915  conjmul 5937  eqneg 5945  2times 6150  modadd1 6477  modmul1 6478  icoun 6540  snunioo 6542  om2uzsuci 6659  cardfz 6671  seq1lem1 6674  seq1res 6692  ser1add2i 6703  ser1addi 6704  seq1shftid 6721  seqzfveq 6749  expp1 6769  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  binom2 6847  sq01 6848  sqrthi 6900  sqrmuli 6906  sqrsq 6923  sqsqr 6924  cjreb 7001  cjmulval 7003  reneg 7005  readd 7006  imneg 7008  imadd 7009  cjcj 7012  cjadd 7013  cjmul 7014  cjneg 7015  addcj 7016  cjexp 7018  absval2 7054  absmul 7060  absdiv 7062  absid 7064  absexp 7070  cjdiv 7092  abssub 7097  recan 7108  abslem2 7112  caurei 7130  cauimi 7131  ser1absdiflem 7132  bcpasc2 7171  bcpasc 7173  fsum1slem 7211  fsump1slem 7215  fsum1ps 7221  fsumadd 7225  csbfsumlem 7229  csbfsum 7230  fsumcom 7231  fsumrev 7232  fsummulc1 7236  fsumconst 7241  serzmulci 7261  serzrelem 7264  binomlem6 7274  bcxmas 7279  climshft2i 7309  iserzshft2i 7310  climaddlem1 7317  climmullem6 7328  ser1consti 7374  cvgcmp2lem 7383  isumnn0nnai 7412  geoseri 7439  fsum0diag 7463  fsum0diag4 7466  efcj 7542  efadd 7572  efexp 7577  ef4p 7608  sinadd 7661  cosadd 7662  demoivre 7695  iscaunns 8155  isgrp 8254  grpass 8260  grpidinvlem3 8263  grpidinv 8265  grpideu 8266  grpidval 8275  grpidinv2 8277  grpinvfval 8283  isgrp2i 8293  gxnn0suc 8320  gxcom 8325  gxinv 8326  gxnn0add 8330  gxnn0mul 8333  isabl 8342  ablcom 8344  gxdi 8355  issubgilem 8363  cnid 8368  ghgrpilem1 8374  ghgrpilem4 8377  ghgrpi 8378  isring 8382  ringi 8383  ringid 8386  ringideu 8387  ringdi 8388  ringdir 8389  ringass 8390  ringsn 8405  vci 8414  vcid 8417  vcdi 8418  vcdir 8419  vcass 8420  isvclem 8443  isnvlem 8476  nvi 8480  nvmeq0 8531  nvs 8537  imsmetlem 8570  vacnlem1 8582  islno 8668  lnolin 8669  ishmo 8726  isphg 8732  phpar2 8738  phpar 8739  ipdiri 8745  ipasslem1 8746  ipasslem5 8750  ipasslem11 8756  ipassi 8757  ipdir 8758  ipass 8761  ip2eqi 8773  minveclem6 8810  minveclem7 8811  minveclem8 8812  htthlem2 8883  isps 8907  sineq0re 8985  hvsubsub4 9202  hvnegdi 9209  hvaddcan 9212  hvaddcan2 9213  hvsubcan 9217  hvsubcan2 9218  hvaddsub4 9221  hial2eq 9248  normlem9at 9263  normsq 9277  norm-iii 9283  normsub 9286  normpyth 9288  normpar 9298  polid 9302  chocunii 9448  pjthlem8 9502  ococ 9524  axpjpj 9532  chj0 9696  chlejb1 9711  chdmm1 9724  chjass 9732  spanun 9744  spansn 9758  elspansn2 9766  cmbr 9803  cmbr3 9827  pjoml2 9830  pjoml3 9831  osum 9866  spansnj 9870  pjch1 9893  pjadji 9908  pjaddi 9909  pjinormi 9910  pjsubi 9911  pjmuli 9912  pjcjt2 9915  pjch 9917  pjopyth 9943  pjpyth 9948  hoaddcom 9980  hoaddass 9988  hocsubdir 9991  hoaddid1 9997  ho0sub 10003  honegsub 10005  adjsym 10039  eigrei 10040  eigre 10041  eigposi 10042  eigorth 10044  ellnop 10064  elhmop 10080  ellnfn 10090  cnvadj 10096  hhlnoi 10106  lnopl 10118  unop 10119  hmop 10126  lnfnl 10135  adj1 10137  eleigvec 10161  hoddi 10194  lnopeq0lem2 10210  lnopunilem1 10214  lnopunilem2 10215  lnopunii 10216  elunop2 10217  lnophmi 10222  lnfnmul 10256  cnlnadjlem5 10283  branmfn 10317  branmfnOLD 10318  hmopidmchi 10359  hmopidmpji 10360  hmopidmch 10361  hmopidmpj 10362  pjss2coi 10372  pjssmi 10373  pjssge0i 10374  pjidmco 10389  pjhmopidm 10390  dfpjop 10391  stel 10422  hstel 10423  hstel2 10427  stj 10443  mdbr 10502  mdi 10503  mdbr3 10505  dmdbr 10507  dmdmd 10508  dmdi 10510  dmdbr3 10513  mddmd2 10517  mdsl1i 10529  chjatom 10565  elghomlem2 10668  ghomgrpilem1 10670  ghomlin 10678  cayleylem2 10695  erdisj2 10731  moec 10745  intprd 10755  njtlc 10804  islatalg 10831  labss1 10837  labss2 10839  isass 10890  opidon 10898  exidu1 10902  cmpidelt 10906  smgrpass2 10914  seqzp2 10918  mndass2 10932  iscom2 10940  com2i 10941  rngmgmbs4 10945  ununr 10955  zrdivrng 10969  vri 10981  limfillem2 11102  iscon 11126  iscon2 11127  clindistop2 11132  isded 11190  dedi 11191  1ded 11192  idosd 11198  domcmpd 11200  codcmpd 11201  iscat 11208  cati 11209  1cat 11213  cmpasso 11227  cmpida 11228  cmpidb 11229  ismona 11264  ismonb 11265  idmon 11272  isepia 11274  isepib 11275  cinvlem1 11282  cinvlem2 11283  isfuna 11288  isfunb 11289  cbvcsb 11397  fictb 11423  ordiso 11426  opnregcld 11467  cldregopn 11468  compsub 11488  topfneec 11562  comppfsc 11578  ist1-3 11604  fgf 11632  fcluscf 11724  isgalem 11771  gagrpid 11780  gaass 11781  upixp 11823  erthdmg 11824  sdclem1 11875  sdc 11877  isumshft2 11893  mettrifi 11912  mettrifi2 11913  caushft 11916  isbnd 11995  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem11 12021  heiborlem32 12042  heiborlem35 12045  bfplem8 12061  bfplem10 12063  phtpycom 12092  phtpycolem2 12094  phtpycolem3 12095  phtpycolem4 12096  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

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

Copyright terms: Public domain