Theorem eqeq12d 2211

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  cdeqeq  2984  sbceqg  3100  csbing  3371  uniprg  3855  unisng  3857  intprg  3908  iununir  4001  csbopabg  4112  undifexmid  4227  exmidundif  4240  exmidundifim  4241  limeq  4413  onsucuni2  4601  ordpwsucexmid  4607  csbima12g  5031  dmsnsnsng  5148  cnvsng  5156  csbiotag  5252  fvmptf  5657  eqfnfv2f  5666  fvreseq  5668  fmptco  5731  fnressn  5751  fvsng  5761  cocan1  5837  cocan2  5838  fliftfun  5846  csbriotag  5893  oveqrspc2v  5952  csbov123g  5964  eqfnov  6033  ovmpos  6050  ov2gf  6051  ovmpodxf  6052  caovcomg  6083  caovassg  6086  caovcang  6089  caovcanrd  6091  caovcan  6092  caovdig  6102  caovdirg  6105  caovimo  6121  offveqb  6159  caofid0l  6166  caofid0r  6167  op1stg  6217  op2ndg  6218  f1o2ndf1  6295  tfrlem1  6375  tfrlem3ag  6376  tfrlem3a  6377  tfrlem5  6381  tfrlem9  6386  tfr0dm  6389  tfrlemiubacc  6397  tfrlemiex  6398  tfrlemi1  6399  tfr1onlem3ag  6404  tfr1onlemubacc  6413  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemubacc  6426  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  tfri3  6434  rdg0g  6455  frecrdg  6475  nna0r  6545  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  ecopovtrn  6700  ecopovsymg  6702  ecopovtrng  6703  ecovcom  6710  ecovicom  6711  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  dom2lem  6840  ordiso2  7110  inl11  7140  updjud  7157  omp1eomlem  7169  difinfsnlem  7174  nnnninfeq  7203  nninfwlporlemd  7247  nninfwlpor  7249  nninfinfwlpo  7255  exmidfodomrlemrALT  7284  exmidaclem  7293  addcanpig  7420  mulcanpig  7421  mulcmpblnq  7454  mulpipqqs  7459  ordpipqqs  7460  mulidnq  7475  enq0sym  7518  nqnq0  7527  mulcmpblnq0  7530  distrnq0  7545  mulcomnq0  7546  addassnq0  7548  nq02m  7551  genipv  7595  cauappcvgprlemladd  7744  addcmpblnr  7825  0idsr  7853  1idsr  7854  axaddcom  7956  ax1rid  7963  ax0id  7964  rereceu  7975  axcaucvg  7986  mulrid  8042  readdcan  8185  cnegexlem1  8220  cnegexlem3  8222  addcan  8225  addcan2  8226  apti  8668  mulcanapd  8707  mulcanap2d  8708  div11ap  8746  divmuleqap  8763  conjmulap  8775  eqneg  8778  cnref1o  9744  fzsuc2  10173  fzprval  10176  fztpval  10177  qtri3or  10349  modqadd1  10472  modqmul1  10488  addmodlteq  10509  frec2uzrdg  10520  frecuzrdgg  10527  seq3val  10571  seqvalcd  10572  seq3fveq2  10586  seqfveq2g  10588  seqfveqg  10589  seq3fveq  10590  seq3feq  10591  seq3shft2  10592  seqshft2g  10593  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqk  10618  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1olemp  10626  seq3f1oleml  10627  seqf1oglem2a  10629  seqf1oglem2  10631  seqf1og  10632  seq3id  10636  seq3id2  10637  seq3homo  10638  seqhomog  10641  seqfeq4g  10642  mulexp  10689  expadd  10692  expmul  10695  modqexp  10777  nn0opth2d  10834  bcpasc  10877  hashennn  10891  hashen  10895  omgadd  10913  hashfzo  10933  hashfzp1  10935  hashxp  10937  hashfacen  10947  seq3coll  10953  shftvalg  11020  shftval4g  11021  replim  11043  cjreb  11050  cjexp  11077  absexp  11263  recan  11293  minclpr  11421  mingeb  11426  sumeq2  11543  zsumdc  11568  fsum3  11571  fsumf1o  11574  fsum3cvg2  11578  fsumadd  11590  isummulc2  11610  fsum2d  11619  fsummulc2  11632  fsumconst  11638  modfsummod  11642  fsumparts  11654  fsumrelem  11655  fsumiun  11661  binom  11668  bcxmas  11673  isumshft  11674  isumnn0nn  11677  mertenslem2  11720  clim2prod  11723  prodfrecap  11730  prodeq2  11741  zproddc  11763  fprodseq  11767  fprodf1o  11772  prodsnf  11776  fprodfac  11799  fprodabs  11800  fprodconst  11804  fprod2d  11807  fprodrec  11813  fprodmodd  11825  efne0  11862  efexp  11866  demoivreALT  11958  moddvds  11983  bitsinv1  12146  gcddiv  12213  alginv  12242  algfx  12247  lcmneg  12269  lcmid  12275  lcmgcdeq  12278  divgcdcoprm0  12296  cncongr1  12298  cncongr2  12299  nn0gcdsq  12395  crth  12419  eulerthlema  12425  eulerthlemh  12426  pythagtriplem1  12461  pcqmul  12499  pcexp  12505  pcneg  12521  pcmpt  12539  pcfac  12546  1arith  12563  setscomd  12746  ercpbllemg  13034  mgmidmo  13076  mgmlrid  13083  lidrideqd  13085  lidrididd  13086  grpinvalem  13089  grpinva  13090  issgrp  13107  isnsgrp  13110  sgrpass  13112  sgrp1  13115  issgrpd  13116  sgrppropd  13117  ismndd  13141  mndpropd  13144  imasmnd2  13156  mnd1  13159  mnd1id  13160  ismhm  13165  mhmpropd  13170  mhmlin  13171  mhmeql  13196  isgrp  13210  grppropd  13221  isgrpd2e  13224  dfgrp2  13231  isgrpid2  13244  grpidd2  13245  grpinvfvalg  13246  grpinvpropdg  13279  grpidssd  13280  grpinvssd  13281  grpsubrcan  13285  dfgrp3mlem  13302  grplactcnv  13306  imasgrp2  13318  mhmlem  13322  mulgnn0p1  13341  mulgaddcom  13354  mulginvcom  13355  mulgneg2  13364  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mhmmulg  13371  isghm  13451  ghmlin  13456  ghmeql  13475  iscmn  13501  cmnpropd  13503  iscmnd  13506  abladdsub4  13522  imasabl  13544  gsumfzconst  13549  isrng  13568  rngass  13573  rngdi  13574  rngdir  13575  rngpropd  13589  imasrng  13590  issrg  13599  srgmulgass  13623  srgpcomp  13624  srg1expzeq1  13629  isring  13634  iscrng2  13649  ringpropd  13672  ringinvnz1ne0  13683  mulgass2  13692  ring1  13693  imasring  13698  opprnegg  13717  dvdsrd  13728  dvreq1  13776  rhmmul  13798  isrhm2d  13799  rhmopp  13810  rhmunitinv  13812  islring  13826  rrgval  13896  unitrrg  13901  opprdomnbg  13908  islmod  13925  lmodlema  13926  islmodd  13927  lmodvsmmulgdi  13957  lmodprop2d  13982  rmodislmodlem  13984  rmodislmod  13985  rnglidlmsgrp  14131  rnglidlrng  14132  quscrng  14167  cnfldmulg  14210  cnfldexp  14211  gsumfzfsumlemm  14221  zndvds  14283  znf1o  14285  znunit  14293  psr1clfi  14322  txcnp  14615  cnmpt11  14627  cnmpt21  14635  cnmptcom  14642  isxms  14795  xmspropd  14821  bdmopn  14848  dvexp  15055  dvmptfsum  15069  rpcxpmul2  15257  wilthlem1  15324  mpodvdsmulf1o  15334  fsumdvdsmul  15335  perfect  15345  lgsne0  15387  gausslemma2d  15418  lgseisenlem2  15420  lgsquad2lem2  15431  2lgslem1a  15437  2lgslem1b  15438  nninffeq  15775