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  8430  cnegexlem1  8465  cnegexlem3  8467  addcan  8470  addcan2  8471  apti  8914  mulcanapd  8953  mulcanap2d  8954  div11ap  8994  divmuleqap  9011  conjmulap  9023  eqneg  9026  cnref1o  10004  fzsuc2  10438  fzprval  10441  fztpval  10442  qtri3or  10627  modqadd1  10750  modqmul1  10766  addmodlteq  10787  frec2uzrdg  10798  frecuzrdgg  10805  seq3val  10849  seqvalcd  10850  seq3fveq2  10864  seqfveq2g  10866  seqfveqg  10867  seq3fveq  10868  seq3feq  10869  seq3shft2  10870  seqshft2g  10871  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seqcaopr3g  10881  seq3caopr2  10882  seqcaopr2g  10883  iseqf1olemkle  10886  iseqf1olemklt  10887  iseqf1olemqk  10896  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1olemp  10904  seq3f1oleml  10905  seqf1oglem2a  10907  seqf1oglem2  10909  seqf1og  10910  seq3id  10914  seq3id2  10915  seq3homo  10916  seqhomog  10919  seqfeq4g  10920  mulexp  10967  expadd  10970  expmul  10973  modqexp  11056  nn0opth2d  11113  bcpasc  11156  bcm1n  11159  hashennn  11171  hashen  11175  omgadd  11194  hashfzo  11215  hashfzp1  11217  hashxp  11219  hashmap  11220  hashfibclem  11234  hashfibc  11235  hashfacen  11236  seq3coll  11242  eqs1  11344  swrdspsleq  11387  pfxeq  11416  pfxsuff1eqwrdeq  11419  ccatopth2  11437  cats1un  11441  swrdccatin1  11445  swrdccat3blem  11459  shftvalg  11549  shftval4g  11550  replim  11572  cjreb  11579  cjexp  11606  absexp  11793  recan  11823  minclpr  11951  mingeb  11956  sumeq2  12073  zsumdc  12099  fsum3  12102  fsumf1o  12105  fsum3cvg2  12109  fsumadd  12121  isummulc2  12141  fsum2d  12150  fsummulc2  12163  fsumconst  12169  modfsummod  12173  fsumparts  12185  fsumrelem  12186  fsumiun  12192  binom  12199  bcxmas  12204  isumshft  12205  isumnn0nn  12208  mertenslem2  12251  clim2prod  12254  prodfrecap  12261  prodeq2  12272  zproddc  12294  fprodseq  12298  fprodf1o  12303  prodsnf  12307  fprodfac  12330  fprodabs  12331  fprodconst  12335  fprod2d  12338  fprodrec  12344  fprodmodd  12356  efne0  12393  efexp  12397  demoivreALT  12489  moddvds  12514  bitsinv1  12677  gcddiv  12744  alginv  12773  algfx  12778  lcmneg  12800  lcmid  12806  lcmgcdeq  12809  divgcdcoprm0  12827  cncongr1  12829  cncongr2  12830  nn0gcdsq  12926  crth  12950  eulerthlema  12956  eulerthlemh  12957  pythagtriplem1  12992  pcqmul  13030  pcexp  13036  pcneg  13052  pcmpt  13070  pcfac  13077  1arith  13094  setscomd  13341  ercpbllemg  13598  mgmidmo  13639  mgmlrid  13646  lidrideqd  13648  lidrididd  13649  grpinvalem  13652  grpinva  13653  issgrp  13670  isnsgrp  13673  sgrpass  13675  sgrp1  13678  issgrpd  13679  sgrppropd  13680  ismndd  13702  mndpropd  13705  imasmnd2  13711  mnd1  13714  mnd1id  13715  ismhm  13720  mhmpropd  13725  mhmlin  13726  mhmeql  13751  isgrp  13765  grppropd  13776  isgrpd2e  13779  dfgrp2  13786  isgrpid2  13799  grpidd2  13800  grpinvfvalg  13801  grpinvpropdg  13834  grpidssd  13835  grpinvssd  13836  grpsubrcan  13840  dfgrp3mlem  13857  grplactcnv  13861  imasgrp2  13867  mhmlem  13871  mulgnn0p1  13890  mulgaddcom  13903  mulginvcom  13904  mulgneg2  13913  mulgnnass  13914  mulgnn0ass  13915  mulgass  13916  mhmmulg  13920  isghm  14000  ghmlin  14005  ghmeql  14024  iscmn  14050  cmnpropd  14052  iscmnd  14055  abladdsub4  14071  imasabl  14093  gsumfzconst  14098  isrng  14177  rngass  14182  rngdi  14183  rngdir  14184  rngpropd  14198  imasrng  14199  issrg  14212  srgmulgass  14236  srgpcomp  14237  srg1expzeq1  14242  isring  14247  iscrng2  14262  ringpropd  14285  ringinvnz1ne0  14296  mulgass2  14305  ring1  14306  imasring  14311  opprnegg  14331  dvdsrd  14343  dvreq1  14391  rhmmul  14413  isrhm2d  14414  rhmopp  14425  rhmunitinv  14427  islring  14441  opprlring  14446  rrgval  14512  unitrrg  14518  opprdomnbg  14525  islmod  14569  lmodlema  14570  islmodd  14571  lmodvsmmulgdi  14601  lmodprop2d  14626  rmodislmodlem  14628  rmodislmod  14629  rnglidlmsgrp  14775  rnglidlrng  14776  quscrng  14811  cnfldmulg  14854  cnfldexp  14855  gsumfzfsumlemm  14865  zndvds  14927  znf1o  14929  znunit  14937  psr1clfi  14973  txcnp  15266  cnmpt11  15278  cnmpt21  15286  cnmptcom  15293  isxms  15446  xmspropd  15472  bdmopn  15499  dvexp  15706  dvmptfsum  15720  rpcxpmul2  15908  wilthlem1  15978  mpodvdsmulf1o  15988  fsumdvdsmul  15989  perfect  15999  lgsne0  16041  gausslemma2d  16072  lgseisenlem2  16074  lgsquad2lem2  16085  2lgslem1a  16091  2lgslem1b  16092  usgredg2v  16349  issubgr  16382  wkslem1  16445  wkslem2  16446  iswlk  16448  uspgr2wlkeq  16490  2wlklem  16501  wlkres  16504  eupth2lem3fi  16601  eupth2fi  16604  depindlem1  16631  depindlem2  16632  depindlem3  16633  depind  16634  nninffeq  16938