Theorem eqeq12d 2249

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 2247	. 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 2216

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

This theorem is referenced by:  cdeqeq  3040  sbceqg  3157  csbing  3432  uniprg  3934  unisng  3936  intprg  3987  iununir  4080  csbopabg  4193  undifexmid  4311  exmidundif  4324  exmidundifim  4325  limeq  4503  onsucuni2  4691  ordpwsucexmid  4697  csbima12g  5128  dmsnsnsng  5245  cnvsng  5253  csbiotag  5350  fvmptf  5775  eqfnfv2f  5784  fvreseq  5786  fmptco  5848  fnressn  5875  fvsng  5885  cocan1  5966  cocan2  5967  fliftfun  5975  csbriotag  6025  oveqrspc2v  6085  csbov123g  6097  eqfnov  6168  ovmpos  6185  ov2gf  6186  ovmpodxf  6187  caovcomg  6218  caovassg  6221  caovcang  6224  caovcanrd  6226  caovcan  6227  caovdig  6237  caovdirg  6240  caovimo  6256  offveqb  6295  caofid0l  6302  caofid0r  6303  op1stg  6357  op2ndg  6358  f1o2ndf1  6437  tfrlem1  6552  tfrlem3ag  6553  tfrlem3a  6554  tfrlem5  6558  tfrlem9  6563  tfr0dm  6566  tfrlemiubacc  6574  tfrlemiex  6575  tfrlemi1  6576  tfr1onlem3ag  6581  tfr1onlemubacc  6590  tfr1onlemex  6591  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemubacc  6603  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  tfri3  6611  rdg0g  6632  frecrdg  6652  nna0r  6724  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  ecovcom  6889  ecovicom  6890  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  dom2lem  7024  ordiso2  7339  inl11  7369  updjud  7386  omp1eomlem  7398  difinfsnlem  7403  nnnninfeq  7432  nninfwlporlemd  7476  nninfwlpor  7478  nninfinfwlpo  7484  exmidfodomrlemrALT  7519  exmidaclem  7528  addcanpig  7665  mulcanpig  7666  mulcmpblnq  7699  mulpipqqs  7704  ordpipqqs  7705  mulidnq  7720  enq0sym  7763  nqnq0  7772  mulcmpblnq0  7775  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  nq02m  7796  genipv  7840  cauappcvgprlemladd  7989  addcmpblnr  8070  0idsr  8098  1idsr  8099  axaddcom  8201  ax1rid  8208  ax0id  8209  rereceu  8220  axcaucvg  8231  mulrid  8287  readdcan  8429  cnegexlem1  8464  cnegexlem3  8466  addcan  8469  addcan2  8470  apti  8913  mulcanapd  8952  mulcanap2d  8953  div11ap  8991  divmuleqap  9008  conjmulap  9020  eqneg  9023  cnref1o  10001  fzsuc2  10435  fzprval  10438  fztpval  10439  qtri3or  10624  modqadd1  10747  modqmul1  10763  addmodlteq  10784  frec2uzrdg  10795  frecuzrdgg  10802  seq3val  10846  seqvalcd  10847  seq3fveq2  10861  seqfveq2g  10863  seqfveqg  10864  seq3fveq  10865  seq3feq  10866  seq3shft2  10867  seqshft2g  10868  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqk  10893  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem2a  10904  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3id2  10912  seq3homo  10913  seqhomog  10916  seqfeq4g  10917  mulexp  10964  expadd  10967  expmul  10970  modqexp  11053  nn0opth2d  11110  bcpasc  11153  bcm1n  11156  hashennn  11168  hashen  11172  omgadd  11191  hashfzo  11212  hashfzp1  11214  hashxp  11216  hashmap  11217  hashfibclem  11231  hashfibc  11232  hashfacen  11233  seq3coll  11239  eqs1  11341  swrdspsleq  11384  pfxeq  11413  pfxsuff1eqwrdeq  11416  ccatopth2  11434  cats1un  11438  swrdccatin1  11442  swrdccat3blem  11456  shftvalg  11546  shftval4g  11547  replim  11569  cjreb  11576  cjexp  11603  absexp  11789  recan  11819  minclpr  11947  mingeb  11952  sumeq2  12069  zsumdc  12095  fsum3  12098  fsumf1o  12101  fsum3cvg2  12105  fsumadd  12117  isummulc2  12137  fsum2d  12146  fsummulc2  12159  fsumconst  12165  modfsummod  12169  fsumparts  12181  fsumrelem  12182  fsumiun  12188  binom  12195  bcxmas  12200  isumshft  12201  isumnn0nn  12204  mertenslem2  12247  clim2prod  12250  prodfrecap  12257  prodeq2  12268  zproddc  12290  fprodseq  12294  fprodf1o  12299  prodsnf  12303  fprodfac  12326  fprodabs  12327  fprodconst  12331  fprod2d  12334  fprodrec  12340  fprodmodd  12352  efne0  12389  efexp  12393  demoivreALT  12485  moddvds  12510  bitsinv1  12673  gcddiv  12740  alginv  12769  algfx  12774  lcmneg  12796  lcmid  12802  lcmgcdeq  12805  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  nn0gcdsq  12922  crth  12946  eulerthlema  12952  eulerthlemh  12953  pythagtriplem1  12988  pcqmul  13026  pcexp  13032  pcneg  13048  pcmpt  13066  pcfac  13073  1arith  13090  setscomd  13337  ercpbllemg  13627  mgmidmo  13669  mgmlrid  13676  lidrideqd  13678  lidrididd  13679  grpinvalem  13682  grpinva  13683  issgrp  13700  isnsgrp  13703  sgrpass  13705  sgrp1  13708  issgrpd  13709  sgrppropd  13710  ismndd  13734  mndpropd  13737  imasmnd2  13749  mnd1  13752  mnd1id  13753  ismhm  13758  mhmpropd  13763  mhmlin  13764  mhmeql  13789  isgrp  13803  grppropd  13814  isgrpd2e  13817  dfgrp2  13824  isgrpid2  13837  grpidd2  13838  grpinvfvalg  13839  grpinvpropdg  13872  grpidssd  13873  grpinvssd  13874  grpsubrcan  13878  dfgrp3mlem  13895  grplactcnv  13899  imasgrp2  13911  mhmlem  13915  mulgnn0p1  13934  mulgaddcom  13947  mulginvcom  13948  mulgneg2  13957  mulgnnass  13958  mulgnn0ass  13959  mulgass  13960  mhmmulg  13964  isghm  14044  ghmlin  14049  ghmeql  14068  iscmn  14094  cmnpropd  14096  iscmnd  14099  abladdsub4  14115  imasabl  14137  gsumfzconst  14142  isrng  14162  rngass  14167  rngdi  14168  rngdir  14169  rngpropd  14183  imasrng  14184  issrg  14193  srgmulgass  14217  srgpcomp  14218  srg1expzeq1  14223  isring  14228  iscrng2  14243  ringpropd  14266  ringinvnz1ne0  14277  mulgass2  14286  ring1  14287  imasring  14292  opprnegg  14312  dvdsrd  14324  dvreq1  14372  rhmmul  14394  isrhm2d  14395  rhmopp  14406  rhmunitinv  14408  islring  14422  opprlring  14427  rrgval  14493  unitrrg  14499  opprdomnbg  14506  islmod  14551  lmodlema  14552  islmodd  14553  lmodvsmmulgdi  14583  lmodprop2d  14608  rmodislmodlem  14610  rmodislmod  14611  rnglidlmsgrp  14757  rnglidlrng  14758  quscrng  14793  cnfldmulg  14836  cnfldexp  14837  gsumfzfsumlemm  14847  zndvds  14909  znf1o  14911  znunit  14919  psr1clfi  14955  txcnp  15248  cnmpt11  15260  cnmpt21  15268  cnmptcom  15275  isxms  15428  xmspropd  15454  bdmopn  15481  dvexp  15688  dvmptfsum  15702  rpcxpmul2  15890  wilthlem1  15960  mpodvdsmulf1o  15970  fsumdvdsmul  15971  perfect  15981  lgsne0  16023  gausslemma2d  16054  lgseisenlem2  16056  lgsquad2lem2  16067  2lgslem1a  16073  2lgslem1b  16074  usgredg2v  16331  issubgr  16364  wkslem1  16427  wkslem2  16428  iswlk  16430  uspgr2wlkeq  16472  2wlklem  16483  wlkres  16486  eupth2lem3fi  16583  eupth2fi  16586  depindlem1  16613  depindlem2  16614  depindlem3  16615  depind  16616  nninffeq  16910