Theorem eqeq12d 2246

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 2244	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  cdeqeq  3027  sbceqg  3144  csbing  3416  uniprg  3913  unisng  3915  intprg  3966  iununir  4059  csbopabg  4172  undifexmid  4289  exmidundif  4302  exmidundifim  4303  limeq  4480  onsucuni2  4668  ordpwsucexmid  4674  csbima12g  5104  dmsnsnsng  5221  cnvsng  5229  csbiotag  5326  fvmptf  5748  eqfnfv2f  5757  fvreseq  5759  fmptco  5821  fnressn  5848  fvsng  5858  cocan1  5938  cocan2  5939  fliftfun  5947  csbriotag  5995  oveqrspc2v  6055  csbov123g  6067  eqfnov  6138  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  caovcomg  6188  caovassg  6191  caovcang  6194  caovcanrd  6196  caovcan  6197  caovdig  6207  caovdirg  6210  caovimo  6226  offveqb  6264  caofid0l  6271  caofid0r  6272  op1stg  6322  op2ndg  6323  f1o2ndf1  6402  tfrlem1  6517  tfrlem3ag  6518  tfrlem3a  6519  tfrlem5  6523  tfrlem9  6528  tfr0dm  6531  tfrlemiubacc  6539  tfrlemiex  6540  tfrlemi1  6541  tfr1onlem3ag  6546  tfr1onlemubacc  6555  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  tfri3  6576  rdg0g  6597  frecrdg  6617  nna0r  6689  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  ecopovtrn  6844  ecopovsymg  6846  ecopovtrng  6847  ecovcom  6854  ecovicom  6855  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  dom2lem  6988  ordiso2  7277  inl11  7307  updjud  7324  omp1eomlem  7336  difinfsnlem  7341  nnnninfeq  7370  nninfwlporlemd  7414  nninfwlpor  7416  nninfinfwlpo  7422  exmidfodomrlemrALT  7457  exmidaclem  7466  addcanpig  7597  mulcanpig  7598  mulcmpblnq  7631  mulpipqqs  7636  ordpipqqs  7637  mulidnq  7652  enq0sym  7695  nqnq0  7704  mulcmpblnq0  7707  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  nq02m  7728  genipv  7772  cauappcvgprlemladd  7921  addcmpblnr  8002  0idsr  8030  1idsr  8031  axaddcom  8133  ax1rid  8140  ax0id  8141  rereceu  8152  axcaucvg  8163  mulrid  8219  readdcan  8362  cnegexlem1  8397  cnegexlem3  8399  addcan  8402  addcan2  8403  apti  8845  mulcanapd  8884  mulcanap2d  8885  div11ap  8923  divmuleqap  8940  conjmulap  8952  eqneg  8955  cnref1o  9928  fzsuc2  10357  fzprval  10360  fztpval  10361  qtri3or  10544  modqadd1  10667  modqmul1  10683  addmodlteq  10704  frec2uzrdg  10715  frecuzrdgg  10722  seq3val  10766  seqvalcd  10767  seq3fveq2  10781  seqfveq2g  10783  seqfveqg  10784  seq3fveq  10785  seq3feq  10786  seq3shft2  10787  seqshft2g  10788  seq3split  10794  seqsplitg  10795  seq3caopr3  10797  seqcaopr3g  10798  seq3caopr2  10799  seqcaopr2g  10800  iseqf1olemkle  10803  iseqf1olemklt  10804  iseqf1olemqk  10813  seq3f1olemqsum  10819  seq3f1olemstep  10820  seq3f1olemp  10821  seq3f1oleml  10822  seqf1oglem2a  10824  seqf1oglem2  10826  seqf1og  10827  seq3id  10831  seq3id2  10832  seq3homo  10833  seqhomog  10836  seqfeq4g  10837  mulexp  10884  expadd  10887  expmul  10890  modqexp  10972  nn0opth2d  11029  bcpasc  11072  hashennn  11086  hashen  11090  omgadd  11109  hashfzo  11130  hashfzp1  11132  hashxp  11134  hashfacen  11144  seq3coll  11150  eqs1  11252  swrdspsleq  11295  pfxeq  11324  pfxsuff1eqwrdeq  11327  ccatopth2  11345  cats1un  11349  swrdccatin1  11353  swrdccat3blem  11367  shftvalg  11457  shftval4g  11458  replim  11480  cjreb  11487  cjexp  11514  absexp  11700  recan  11730  minclpr  11858  mingeb  11863  sumeq2  11980  zsumdc  12006  fsum3  12009  fsumf1o  12012  fsum3cvg2  12016  fsumadd  12028  isummulc2  12048  fsum2d  12057  fsummulc2  12070  fsumconst  12076  modfsummod  12080  fsumparts  12092  fsumrelem  12093  fsumiun  12099  binom  12106  bcxmas  12111  isumshft  12112  isumnn0nn  12115  mertenslem2  12158  clim2prod  12161  prodfrecap  12168  prodeq2  12179  zproddc  12201  fprodseq  12205  fprodf1o  12210  prodsnf  12214  fprodfac  12237  fprodabs  12238  fprodconst  12242  fprod2d  12245  fprodrec  12251  fprodmodd  12263  efne0  12300  efexp  12304  demoivreALT  12396  moddvds  12421  bitsinv1  12584  gcddiv  12651  alginv  12680  algfx  12685  lcmneg  12707  lcmid  12713  lcmgcdeq  12716  divgcdcoprm0  12734  cncongr1  12736  cncongr2  12737  nn0gcdsq  12833  crth  12857  eulerthlema  12863  eulerthlemh  12864  pythagtriplem1  12899  pcqmul  12937  pcexp  12943  pcneg  12959  pcmpt  12977  pcfac  12984  1arith  13001  setscomd  13184  ercpbllemg  13474  mgmidmo  13516  mgmlrid  13523  lidrideqd  13525  lidrididd  13526  grpinvalem  13529  grpinva  13530  issgrp  13547  isnsgrp  13550  sgrpass  13552  sgrp1  13555  issgrpd  13556  sgrppropd  13557  ismndd  13581  mndpropd  13584  imasmnd2  13596  mnd1  13599  mnd1id  13600  ismhm  13605  mhmpropd  13610  mhmlin  13611  mhmeql  13636  isgrp  13650  grppropd  13661  isgrpd2e  13664  dfgrp2  13671  isgrpid2  13684  grpidd2  13685  grpinvfvalg  13686  grpinvpropdg  13719  grpidssd  13720  grpinvssd  13721  grpsubrcan  13725  dfgrp3mlem  13742  grplactcnv  13746  imasgrp2  13758  mhmlem  13762  mulgnn0p1  13781  mulgaddcom  13794  mulginvcom  13795  mulgneg2  13804  mulgnnass  13805  mulgnn0ass  13806  mulgass  13807  mhmmulg  13811  isghm  13891  ghmlin  13896  ghmeql  13915  iscmn  13941  cmnpropd  13943  iscmnd  13946  abladdsub4  13962  imasabl  13984  gsumfzconst  13989  isrng  14009  rngass  14014  rngdi  14015  rngdir  14016  rngpropd  14030  imasrng  14031  issrg  14040  srgmulgass  14064  srgpcomp  14065  srg1expzeq1  14070  isring  14075  iscrng2  14090  ringpropd  14113  ringinvnz1ne0  14124  mulgass2  14133  ring1  14134  imasring  14139  opprnegg  14158  dvdsrd  14170  dvreq1  14218  rhmmul  14240  isrhm2d  14241  rhmopp  14252  rhmunitinv  14254  islring  14268  rrgval  14338  unitrrg  14343  opprdomnbg  14350  islmod  14367  lmodlema  14368  islmodd  14369  lmodvsmmulgdi  14399  lmodprop2d  14424  rmodislmodlem  14426  rmodislmod  14427  rnglidlmsgrp  14573  rnglidlrng  14574  quscrng  14609  cnfldmulg  14652  cnfldexp  14653  gsumfzfsumlemm  14663  zndvds  14725  znf1o  14727  znunit  14735  psr1clfi  14769  txcnp  15062  cnmpt11  15074  cnmpt21  15082  cnmptcom  15089  isxms  15242  xmspropd  15268  bdmopn  15295  dvexp  15502  dvmptfsum  15516  rpcxpmul2  15704  wilthlem1  15774  mpodvdsmulf1o  15784  fsumdvdsmul  15785  perfect  15795  lgsne0  15837  gausslemma2d  15868  lgseisenlem2  15870  lgsquad2lem2  15881  2lgslem1a  15887  2lgslem1b  15888  usgredg2v  16145  issubgr  16178  wkslem1  16241  wkslem2  16242  iswlk  16244  uspgr2wlkeq  16286  2wlklem  16297  wlkres  16300  eupth2lem3fi  16397  eupth2fi  16400  depindlem1  16427  depindlem2  16428  depindlem3  16429  depind  16430  nninffeq  16726