Theorem eqeq12d 2253

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3950  unisng  3952  intprg  4003  iununir  4096  csbopabg  4210  undifexmid  4332  exmidundif  4345  exmidundifim  4346  limeq  4524  onsucuni2  4713  ordpwsucexmid  4719  csbima12g  5151  dmsnsnsng  5268  cnvsng  5276  csbiotag  5373  fvmptf  5801  eqfnfv2f  5813  fvreseq  5815  fmptco  5877  fnressn  5904  fvsng  5914  cocan1  5996  cocan2  5997  fliftfun  6005  csbriotag  6055  oveqrspc2v  6115  csbov123g  6127  eqfnov  6198  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  caovcomg  6248  caovassg  6251  caovcang  6254  caovcanrd  6256  caovcan  6257  caovdig  6267  caovdirg  6270  caovimo  6286  offveqb  6326  caofid0l  6333  caofid0r  6334  op1stg  6388  op2ndg  6389  f1o2ndf1  6468  tfrlem1  6584  tfrlem3ag  6585  tfrlem3a  6586  tfrlem5  6590  tfrlem9  6595  tfr0dm  6598  tfrlemiubacc  6606  tfrlemiex  6607  tfrlemi1  6608  tfr1onlem3ag  6613  tfr1onlemubacc  6622  tfr1onlemex  6623  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemubacc  6635  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  tfri3  6643  rdg0g  6664  frecrdg  6684  nna0r  6756  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  ecopovtrn  6911  ecopovsymg  6913  ecopovtrng  6914  ecovcom  6921  ecovicom  6922  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  dom2lem  7064  ordiso2  7382  inl11  7412  updjud  7429  omp1eomlem  7441  difinfsnlem  7446  nnnninfeq  7475  nninfwlporlemd  7519  nninfwlpor  7521  nninfinfwlpo  7527  exmidfodomrlemrALT  7562  exmidaclem  7571  addcanpig  7708  mulcanpig  7709  mulcmpblnq  7742  mulpipqqs  7747  ordpipqqs  7748  mulidnq  7763  enq0sym  7806  nqnq0  7815  mulcmpblnq0  7818  distrnq0  7833  mulcomnq0  7834  addassnq0  7836  nq02m  7839  genipv  7883  cauappcvgprlemladd  8032  addcmpblnr  8113  0idsr  8141  1idsr  8142  axaddcom  8244  ax1rid  8251  ax0id  8252  rereceu  8263  axcaucvg  8274  mulrid  8330  readdcan  8474  cnegexlem1  8509  cnegexlem3  8511  addcan  8514  addcan2  8515  apti  8959  mulcanapd  8998  mulcanap2d  8999  div11ap  9039  divmuleqap  9056  conjmulap  9068  eqneg  9071  ofsubeq0  9301  cnref1o  10068  fzsuc2  10503  fzprval  10506  fztpval  10507  qtri3or  10692  modqadd1  10819  modqmul1  10835  addmodlteq  10856  frec2uzrdg  10867  frecuzrdgg  10874  seq3val  10918  seqvalcd  10919  seq3fveq2  10933  seqfveq2g  10935  seqfveqg  10936  seq3fveq  10937  seq3feq  10938  seq3shft2  10939  seqshft2g  10940  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqk  10965  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  seq3f1oleml  10974  seqf1oglem2a  10976  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3id2  10984  seq3homo  10985  seqhomog  10988  seqfeq4g  10989  mulexp  11036  expadd  11039  expmul  11042  modqexp  11125  nn0opth2d  11183  bcpasc  11226  bcm1n  11229  hashennn  11241  hashen  11245  omgadd  11264  hashfzo  11285  hashfzp1  11287  hashxp  11289  hashmap  11290  hashfibclem  11304  hashfibc  11305  hashfacen  11306  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  seq3coll  11316  eqs1  11418  swrdspsleq  11461  pfxeq  11490  pfxsuff1eqwrdeq  11493  ccatopth2  11511  cats1un  11515  swrdccatin1  11519  swrdccat3blem  11533  shftvalg  11623  shftval4g  11624  replim  11646  cjreb  11653  cjexp  11680  absexp  11868  recan  11898  minclpr  12027  mingeb  12033  sumeq2  12150  zsumdc  12176  fsum3  12179  fsumf1o  12182  fsum3cvg2  12186  fsumadd  12198  isummulc2  12218  fsum2d  12227  fsummulc2  12240  fsumconst  12246  modfsummod  12250  fsumparts  12262  fsumrelem  12263  fsumiun  12269  binom  12276  bcxmas  12281  isumshft  12282  isumnn0nn  12285  mertenslem2  12328  clim2prod  12331  prodfrecap  12338  prodeq2  12349  zproddc  12371  fprodseq  12375  fprodf1o  12380  prodsnf  12384  fprodfac  12407  fprodabs  12408  fprodconst  12412  fprod2d  12415  fprodrec  12421  fprodmodd  12433  efne0  12470  efexp  12474  demoivreALT  12566  moddvds  12591  bitsinv1  12754  gcddiv  12821  alginv  12850  algfx  12855  lcmneg  12877  lcmid  12883  lcmgcdeq  12886  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  nn0gcdsq  13005  crth  13031  eulerthlema  13037  eulerthlemh  13038  pythagtriplem1  13073  pcqmul  13111  pcexp  13117  pcneg  13133  pcmpt  13151  pcfac  13158  1arith  13175  setscomd  13451  ercpbllemg  13710  mgmidmo  13751  mgmlrid  13758  lidrideqd  13760  lidrididd  13761  grpinvalem  13764  grpinva  13765  issgrp  13777  isnsgrp  13780  sgrpass  13782  sgrp1  13785  issgrpd  13786  sgrppropd  13787  ismndd  13809  mndpropd  13812  imasmnd2  13818  mnd1  13821  mnd1id  13822  ismhm  13827  mhmpropd  13832  mhmlin  13833  mhmeql  13858  isgrp  13870  grppropd  13881  isgrpd2e  13884  dfgrp2  13891  isgrpid2  13904  grpidd2  13905  grpinvfvalg  13906  grpinvpropdg  13939  grpidssd  13940  grpinvssd  13941  grpsubrcan  13945  dfgrp3mlem  13962  grplactcnv  13966  imasgrp2  13972  mhmlem  13976  mulgnn0p1  13995  mulgaddcom  14008  mulginvcom  14009  mulgneg2  14018  mulgnnass  14019  mulgnn0ass  14020  mulgass  14021  mhmmulg  14025  isghm  14105  ghmlin  14110  ghmeql  14129  cntzex  14150  cntzfval  14152  elcntz  14154  cntzsnval  14156  elcntzsn  14157  cntzi  14162  resscntz  14166  cntzmhm  14173  iscmn  14186  cmnpropd  14188  iscmnd  14191  cmnsubm  14202  abladdsub4  14208  imasabl  14230  gzsumconst  14233  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  gsumconstcmn  14266  gsum2dfilem2  14272  isrng  14340  rngass  14345  rngdi  14346  rngdir  14347  rngpropd  14361  imasrng  14362  issrg  14376  srgmulgass  14400  srgpcomp  14401  srg1expzeq1  14406  isring  14411  iscrng2  14426  ringpropd  14450  ringinvnz1ne0  14461  mulgass2  14470  ring1  14471  imasring  14478  opprnegg  14498  dvdsrd  14510  dvreq1  14558  rhmmul  14580  isrhm2d  14581  rhmopp  14592  rhmunitinv  14594  islring  14608  opprlring  14613  rrgval  14679  unitrrg  14685  opprdomnbg  14692  islmod  14736  lmodlema  14737  islmodd  14738  lmodvsmmulgdi  14769  lmodprop2d  14794  rmodislmodlem  14796  rmodislmod  14797  rnglidlmsgrp  14943  rnglidlrng  14944  quscrng  14979  cnfldmulg  15022  cnfldexp  15023  gsumfsum  15032  zndvds  15093  znf1o  15095  znunit  15103  isassa  15111  assalem  15112  isassad  15120  assapropd  15123  assamulgscm  15152  psr1clfi  15218  mvrf1fi  15231  txcnp  15530  cnmpt11  15542  cnmpt21  15550  cnmptcom  15557  isxms  15710  xmspropd  15736  bdmopn  15763  dvexp  15970  dvmptfsum  15984  sineq0re  16109  rpcxpmul2  16179  wilthlem1  16265  mpodvdsmulf1o  16317  fsumdvdsmul  16318  perfect  16334  lgsne0  16395  gausslemma2d  16426  lgseisenlem2  16428  lgsquad2lem2  16439  2lgslem1a  16445  2lgslem1b  16446  usgredg2v  16703  issubgr  16736  wkslem1  16799  wkslem2  16800  iswlk  16802  uspgr2wlkeq  16844  2wlklem  16855  wlkres  16858  eupth2lem3fi  16955  eupth2fi  16958  depindlem1  16985  depindlem2  16986  depindlem3  16987  depind  16988  nninffeq  17302