Theorem eqeq12d 2192

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
eqeq12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eqeq12d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		eqeq12 2190	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  cdeqeq  2958  sbceqg  3074  csbing  3343  uniprg  3825  unisng  3827  intprg  3878  iununir  3971  csbopabg  4082  undifexmid  4194  exmidundif  4207  exmidundifim  4208  limeq  4378  onsucuni2  4564  ordpwsucexmid  4570  csbima12g  4990  dmsnsnsng  5107  cnvsng  5115  csbiotag  5210  fvmptf  5609  eqfnfv2f  5618  fvreseq  5620  fmptco  5683  fnressn  5703  fvsng  5713  cocan1  5788  cocan2  5789  fliftfun  5797  csbriotag  5843  oveqrspc2v  5902  csbov123g  5913  eqfnov  5981  ovmpos  5998  ov2gf  5999  ovmpodxf  6000  caovcomg  6030  caovassg  6033  caovcang  6036  caovcanrd  6038  caovcan  6039  caovdig  6049  caovdirg  6052  caovimo  6068  offveqb  6102  op1stg  6151  op2ndg  6152  f1o2ndf1  6229  tfrlem1  6309  tfrlem3ag  6310  tfrlem3a  6311  tfrlem5  6315  tfrlem9  6320  tfr0dm  6323  tfrlemiubacc  6331  tfrlemiex  6332  tfrlemi1  6333  tfr1onlem3ag  6338  tfr1onlemubacc  6347  tfr1onlemex  6348  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemubacc  6360  tfrcllemex  6361  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  tfri3  6368  rdg0g  6389  frecrdg  6409  nna0r  6479  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  ecopovtrn  6632  ecopovsymg  6634  ecopovtrng  6635  ecovcom  6642  ecovicom  6643  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  dom2lem  6772  ordiso2  7034  inl11  7064  updjud  7081  omp1eomlem  7093  difinfsnlem  7098  nnnninfeq  7126  nninfwlporlemd  7170  nninfwlpor  7172  exmidfodomrlemrALT  7202  exmidaclem  7207  addcanpig  7333  mulcanpig  7334  mulcmpblnq  7367  mulpipqqs  7372  ordpipqqs  7373  mulidnq  7388  enq0sym  7431  nqnq0  7440  mulcmpblnq0  7443  distrnq0  7458  mulcomnq0  7459  addassnq0  7461  nq02m  7464  genipv  7508  cauappcvgprlemladd  7657  addcmpblnr  7738  0idsr  7766  1idsr  7767  axaddcom  7869  ax1rid  7876  ax0id  7877  rereceu  7888  axcaucvg  7899  mulrid  7954  readdcan  8097  cnegexlem1  8132  cnegexlem3  8134  addcan  8137  addcan2  8138  apti  8579  mulcanapd  8618  mulcanap2d  8619  div11ap  8657  divmuleqap  8674  conjmulap  8686  eqneg  8689  cnref1o  9650  fzsuc2  10079  fzprval  10082  fztpval  10083  qtri3or  10243  modqadd1  10361  modqmul1  10377  addmodlteq  10398  frec2uzrdg  10409  frecuzrdgg  10416  seq3val  10458  seqvalcd  10459  seq3fveq2  10469  seq3fveq  10471  seq3feq  10472  seq3shft2  10473  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemkle  10484  iseqf1olemklt  10485  iseqf1olemqk  10494  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1olemp  10502  seq3f1oleml  10503  seq3id  10508  seq3id2  10509  seq3homo  10510  mulexp  10559  expadd  10562  expmul  10565  modqexp  10647  nn0opth2d  10703  bcpasc  10746  hashennn  10760  hashen  10764  omgadd  10782  hashfzo  10802  hashfzp1  10804  hashxp  10806  hashfacen  10816  seq3coll  10822  shftvalg  10845  shftval4g  10846  replim  10868  cjreb  10875  cjexp  10902  absexp  11088  recan  11118  minclpr  11245  mingeb  11250  sumeq2  11367  zsumdc  11392  fsum3  11395  fsumf1o  11398  fsum3cvg2  11402  fsumadd  11414  isummulc2  11434  fsum2d  11443  fsummulc2  11456  fsumconst  11462  modfsummod  11466  fsumparts  11478  fsumrelem  11479  fsumiun  11485  binom  11492  bcxmas  11497  isumshft  11498  isumnn0nn  11501  mertenslem2  11544  clim2prod  11547  prodfrecap  11554  prodeq2  11565  zproddc  11587  fprodseq  11591  fprodf1o  11596  prodsnf  11600  fprodfac  11623  fprodabs  11624  fprodconst  11628  fprod2d  11631  fprodrec  11637  fprodmodd  11649  efne0  11686  efexp  11690  demoivreALT  11781  moddvds  11806  gcddiv  12020  alginv  12047  algfx  12052  lcmneg  12074  lcmid  12080  lcmgcdeq  12083  divgcdcoprm0  12101  cncongr1  12103  cncongr2  12104  nn0gcdsq  12200  crth  12224  eulerthlema  12230  eulerthlemh  12231  pythagtriplem1  12265  pcqmul  12303  pcexp  12309  pcneg  12324  pcmpt  12341  pcfac  12348  1arith  12365  setscomd  12503  ercpbllemg  12749  mgmidmo  12791  mgmlrid  12798  lidrideqd  12800  lidrididd  12801  grprinvlem  12804  grprinvd  12805  issgrp  12809  isnsgrp  12812  sgrpass  12814  sgrp1  12816  ismndd  12838  mndpropd  12841  mnd1  12847  mnd1id  12848  ismhm  12853  mhmpropd  12857  mhmlin  12858  mhmeql  12876  isgrp  12883  grppropd  12893  isgrpd2e  12896  dfgrp2  12902  isgrpid2  12913  grpidd2  12914  grpinvfvalg  12915  grpinvpropdg  12945  grpidssd  12946  grpinvssd  12947  grpsubrcan  12951  dfgrp3mlem  12968  grplactcnv  12972  mhmlem  12978  mulgnn0p1  12994  mulgaddcom  13007  mulginvcom  13008  mulgneg2  13017  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mhmmulg  13024  iscmn  13096  cmnpropd  13098  iscmnd  13101  abladdsub4  13117  issrg  13148  srgmulgass  13172  srgpcomp  13173  srg1expzeq1  13178  isring  13183  iscrng2  13198  ringpropd  13217  ringinvnz1ne0  13226  mulgass2  13235  ring1  13236  opprnegg  13253  dvdsrd  13263  dvreq1  13311  islring  13333  islmod  13381  lmodlema  13382  islmodd  13383  lmodvsmmulgdi  13413  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  cnfldmulg  13473  cnfldexp  13474  txcnp  13774  cnmpt11  13786  cnmpt21  13794  cnmptcom  13801  isxms  13954  xmspropd  13980  bdmopn  14007  dvexp  14178  lgsne0  14442  lgseisenlem2  14454  nninffeq  14772