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 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3948  unisng  3950  intprg  4001  iununir  4094  csbopabg  4207  undifexmid  4328  exmidundif  4341  exmidundifim  4342  limeq  4520  onsucuni2  4709  ordpwsucexmid  4715  csbima12g  5146  dmsnsnsng  5263  cnvsng  5271  csbiotag  5368  fvmptf  5795  eqfnfv2f  5804  fvreseq  5806  fmptco  5868  fnressn  5895  fvsng  5905  cocan1  5987  cocan2  5988  fliftfun  5996  csbriotag  6046  oveqrspc2v  6106  csbov123g  6118  eqfnov  6189  ovmpos  6206  ov2gf  6207  ovmpodxf  6208  caovcomg  6239  caovassg  6242  caovcang  6245  caovcanrd  6247  caovcan  6248  caovdig  6258  caovdirg  6261  caovimo  6277  offveqb  6316  caofid0l  6323  caofid0r  6324  op1stg  6378  op2ndg  6379  f1o2ndf1  6458  tfrlem1  6573  tfrlem3ag  6574  tfrlem3a  6575  tfrlem5  6579  tfrlem9  6584  tfr0dm  6587  tfrlemiubacc  6595  tfrlemiex  6596  tfrlemi1  6597  tfr1onlem3ag  6602  tfr1onlemubacc  6611  tfr1onlemex  6612  tfr1onlemaccex  6613  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllemubacc  6624  tfrcllemex  6625  tfrcllemaccex  6626  tfrcllemres  6627  tfrcldm  6628  tfri3  6632  rdg0g  6653  frecrdg  6673  nna0r  6745  nnacom  6751  nnaass  6752  nndi  6753  nnmass  6754  nnmsucr  6755  nnmcom  6756  ecopovtrn  6900  ecopovsymg  6902  ecopovtrng  6903  ecovcom  6910  ecovicom  6911  ecovass  6912  ecoviass  6913  ecovdi  6914  ecovidi  6915  dom2lem  7052  ordiso2  7369  inl11  7399  updjud  7416  omp1eomlem  7428  difinfsnlem  7433  nnnninfeq  7462  nninfwlporlemd  7506  nninfwlpor  7508  nninfinfwlpo  7514  exmidfodomrlemrALT  7549  exmidaclem  7558  addcanpig  7695  mulcanpig  7696  mulcmpblnq  7729  mulpipqqs  7734  ordpipqqs  7735  mulidnq  7750  enq0sym  7793  nqnq0  7802  mulcmpblnq0  7805  distrnq0  7820  mulcomnq0  7821  addassnq0  7823  nq02m  7826  genipv  7870  cauappcvgprlemladd  8019  addcmpblnr  8100  0idsr  8128  1idsr  8129  axaddcom  8231  ax1rid  8238  ax0id  8239  rereceu  8250  axcaucvg  8261  mulrid  8317  readdcan  8460  cnegexlem1  8495  cnegexlem3  8497  addcan  8500  addcan2  8501  apti  8944  mulcanapd  8983  mulcanap2d  8984  div11ap  9024  divmuleqap  9041  conjmulap  9053  eqneg  9056  cnref1o  10034  fzsuc2  10469  fzprval  10472  fztpval  10473  qtri3or  10658  modqadd1  10781  modqmul1  10797  addmodlteq  10818  frec2uzrdg  10829  frecuzrdgg  10836  seq3val  10880  seqvalcd  10881  seq3fveq2  10895  seqfveq2g  10897  seqfveqg  10898  seq3fveq  10899  seq3feq  10900  seq3shft2  10901  seqshft2g  10902  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seqcaopr3g  10912  seq3caopr2  10913  seqcaopr2g  10914  iseqf1olemkle  10917  iseqf1olemklt  10918  iseqf1olemqk  10927  seq3f1olemqsum  10933  seq3f1olemstep  10934  seq3f1olemp  10935  seq3f1oleml  10936  seqf1oglem2a  10938  seqf1oglem2  10940  seqf1og  10941  seq3id  10945  seq3id2  10946  seq3homo  10947  seqhomog  10950  seqfeq4g  10951  mulexp  10998  expadd  11001  expmul  11004  modqexp  11087  nn0opth2d  11144  bcpasc  11187  bcm1n  11190  hashennn  11202  hashen  11206  omgadd  11225  hashfzo  11246  hashfzp1  11248  hashxp  11250  hashmap  11251  hashfibclem  11265  hashfibc  11266  hashfacen  11267  hashf1lem1  11268  hashf1lem2  11269  hashf1  11270  seq3coll  11277  eqs1  11379  swrdspsleq  11422  pfxeq  11451  pfxsuff1eqwrdeq  11454  ccatopth2  11472  cats1un  11476  swrdccatin1  11480  swrdccat3blem  11494  shftvalg  11584  shftval4g  11585  replim  11607  cjreb  11614  cjexp  11641  absexp  11828  recan  11858  minclpr  11986  mingeb  11991  sumeq2  12108  zsumdc  12134  fsum3  12137  fsumf1o  12140  fsum3cvg2  12144  fsumadd  12156  isummulc2  12176  fsum2d  12185  fsummulc2  12198  fsumconst  12204  modfsummod  12208  fsumparts  12220  fsumrelem  12221  fsumiun  12227  binom  12234  bcxmas  12239  isumshft  12240  isumnn0nn  12243  mertenslem2  12286  clim2prod  12289  prodfrecap  12296  prodeq2  12307  zproddc  12329  fprodseq  12333  fprodf1o  12338  prodsnf  12342  fprodfac  12365  fprodabs  12366  fprodconst  12370  fprod2d  12373  fprodrec  12379  fprodmodd  12391  efne0  12428  efexp  12432  demoivreALT  12524  moddvds  12549  bitsinv1  12712  gcddiv  12779  alginv  12808  algfx  12813  lcmneg  12835  lcmid  12841  lcmgcdeq  12844  divgcdcoprm0  12862  cncongr1  12864  cncongr2  12865  nn0gcdsq  12961  crth  12985  eulerthlema  12991  eulerthlemh  12992  pythagtriplem1  13027  pcqmul  13065  pcexp  13071  pcneg  13087  pcmpt  13105  pcfac  13112  1arith  13129  setscomd  13376  ercpbllemg  13634  mgmidmo  13675  mgmlrid  13682  lidrideqd  13684  lidrididd  13685  grpinvalem  13688  grpinva  13689  issgrp  13701  isnsgrp  13704  sgrpass  13706  sgrp1  13709  issgrpd  13710  sgrppropd  13711  ismndd  13733  mndpropd  13736  imasmnd2  13742  mnd1  13745  mnd1id  13746  ismhm  13751  mhmpropd  13756  mhmlin  13757  mhmeql  13782  isgrp  13794  grppropd  13805  isgrpd2e  13808  dfgrp2  13815  isgrpid2  13828  grpidd2  13829  grpinvfvalg  13830  grpinvpropdg  13863  grpidssd  13864  grpinvssd  13865  grpsubrcan  13869  dfgrp3mlem  13886  grplactcnv  13890  imasgrp2  13896  mhmlem  13900  mulgnn0p1  13919  mulgaddcom  13932  mulginvcom  13933  mulgneg2  13942  mulgnnass  13943  mulgnn0ass  13944  mulgass  13945  mhmmulg  13949  isghm  14029  ghmlin  14034  ghmeql  14053  iscmn  14079  cmnpropd  14081  iscmnd  14084  cmnsubm  14095  abladdsub4  14101  imasabl  14123  gzsumconst  14126  gsummptfidmadd  14144  gsumconstcmn  14149  isrng  14216  rngass  14221  rngdi  14222  rngdir  14223  rngpropd  14237  imasrng  14238  issrg  14252  srgmulgass  14276  srgpcomp  14277  srg1expzeq1  14282  isring  14287  iscrng2  14302  ringpropd  14326  ringinvnz1ne0  14337  mulgass2  14346  ring1  14347  imasring  14352  opprnegg  14372  dvdsrd  14384  dvreq1  14432  rhmmul  14454  isrhm2d  14455  rhmopp  14466  rhmunitinv  14468  islring  14482  opprlring  14487  rrgval  14553  unitrrg  14559  opprdomnbg  14566  islmod  14610  lmodlema  14611  islmodd  14612  lmodvsmmulgdi  14643  lmodprop2d  14668  rmodislmodlem  14670  rmodislmod  14671  rnglidlmsgrp  14817  rnglidlrng  14818  quscrng  14853  cnfldmulg  14896  cnfldexp  14897  gsumfsum  14906  zndvds  14967  znf1o  14969  znunit  14977  isassa  14985  assalem  14986  isassad  14994  assapropd  14997  assamulgscm  15026  psr1clfi  15062  txcnp  15355  cnmpt11  15367  cnmpt21  15375  cnmptcom  15382  isxms  15535  xmspropd  15561  bdmopn  15588  dvexp  15795  dvmptfsum  15809  rpcxpmul2  15998  wilthlem1  16077  mpodvdsmulf1o  16087  fsumdvdsmul  16088  perfect  16098  lgsne0  16140  gausslemma2d  16171  lgseisenlem2  16173  lgsquad2lem2  16184  2lgslem1a  16190  2lgslem1b  16191  usgredg2v  16448  issubgr  16481  wkslem1  16544  wkslem2  16545  iswlk  16547  uspgr2wlkeq  16589  2wlklem  16600  wlkres  16603  eupth2lem3fi  16700  eupth2fi  16703  depindlem1  16730  depindlem2  16731  depindlem3  16732  depind  16733  nninffeq  17037