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  exmidfodomrlemrALT  7282  exmidaclem  7291  addcanpig  7418  mulcanpig  7419  mulcmpblnq  7452  mulpipqqs  7457  ordpipqqs  7458  mulidnq  7473  enq0sym  7516  nqnq0  7525  mulcmpblnq0  7528  distrnq0  7543  mulcomnq0  7544  addassnq0  7546  nq02m  7549  genipv  7593  cauappcvgprlemladd  7742  addcmpblnr  7823  0idsr  7851  1idsr  7852  axaddcom  7954  ax1rid  7961  ax0id  7962  rereceu  7973  axcaucvg  7984  mulrid  8040  readdcan  8183  cnegexlem1  8218  cnegexlem3  8220  addcan  8223  addcan2  8224  apti  8666  mulcanapd  8705  mulcanap2d  8706  div11ap  8744  divmuleqap  8761  conjmulap  8773  eqneg  8776  cnref1o  9742  fzsuc2  10171  fzprval  10174  fztpval  10175  qtri3or  10347  modqadd1  10470  modqmul1  10486  addmodlteq  10507  frec2uzrdg  10518  frecuzrdgg  10525  seq3val  10569  seqvalcd  10570  seq3fveq2  10584  seqfveq2g  10586  seqfveqg  10587  seq3fveq  10588  seq3feq  10589  seq3shft2  10590  seqshft2g  10591  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqk  10616  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1olemp  10624  seq3f1oleml  10625  seqf1oglem2a  10627  seqf1oglem2  10629  seqf1og  10630  seq3id  10634  seq3id2  10635  seq3homo  10636  seqhomog  10639  seqfeq4g  10640  mulexp  10687  expadd  10690  expmul  10693  modqexp  10775  nn0opth2d  10832  bcpasc  10875  hashennn  10889  hashen  10893  omgadd  10911  hashfzo  10931  hashfzp1  10933  hashxp  10935  hashfacen  10945  seq3coll  10951  shftvalg  11018  shftval4g  11019  replim  11041  cjreb  11048  cjexp  11075  absexp  11261  recan  11291  minclpr  11419  mingeb  11424  sumeq2  11541  zsumdc  11566  fsum3  11569  fsumf1o  11572  fsum3cvg2  11576  fsumadd  11588  isummulc2  11608  fsum2d  11617  fsummulc2  11630  fsumconst  11636  modfsummod  11640  fsumparts  11652  fsumrelem  11653  fsumiun  11659  binom  11666  bcxmas  11671  isumshft  11672  isumnn0nn  11675  mertenslem2  11718  clim2prod  11721  prodfrecap  11728  prodeq2  11739  zproddc  11761  fprodseq  11765  fprodf1o  11770  prodsnf  11774  fprodfac  11797  fprodabs  11798  fprodconst  11802  fprod2d  11805  fprodrec  11811  fprodmodd  11823  efne0  11860  efexp  11864  demoivreALT  11956  moddvds  11981  bitsinv1  12144  gcddiv  12211  alginv  12240  algfx  12245  lcmneg  12267  lcmid  12273  lcmgcdeq  12276  divgcdcoprm0  12294  cncongr1  12296  cncongr2  12297  nn0gcdsq  12393  crth  12417  eulerthlema  12423  eulerthlemh  12424  pythagtriplem1  12459  pcqmul  12497  pcexp  12503  pcneg  12519  pcmpt  12537  pcfac  12544  1arith  12561  setscomd  12744  ercpbllemg  13032  mgmidmo  13074  mgmlrid  13081  lidrideqd  13083  lidrididd  13084  grpinvalem  13087  grpinva  13088  issgrp  13105  isnsgrp  13108  sgrpass  13110  sgrp1  13113  issgrpd  13114  sgrppropd  13115  ismndd  13139  mndpropd  13142  imasmnd2  13154  mnd1  13157  mnd1id  13158  ismhm  13163  mhmpropd  13168  mhmlin  13169  mhmeql  13194  isgrp  13208  grppropd  13219  isgrpd2e  13222  dfgrp2  13229  isgrpid2  13242  grpidd2  13243  grpinvfvalg  13244  grpinvpropdg  13277  grpidssd  13278  grpinvssd  13279  grpsubrcan  13283  dfgrp3mlem  13300  grplactcnv  13304  imasgrp2  13316  mhmlem  13320  mulgnn0p1  13339  mulgaddcom  13352  mulginvcom  13353  mulgneg2  13362  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  mhmmulg  13369  isghm  13449  ghmlin  13454  ghmeql  13473  iscmn  13499  cmnpropd  13501  iscmnd  13504  abladdsub4  13520  imasabl  13542  gsumfzconst  13547  isrng  13566  rngass  13571  rngdi  13572  rngdir  13573  rngpropd  13587  imasrng  13588  issrg  13597  srgmulgass  13621  srgpcomp  13622  srg1expzeq1  13627  isring  13632  iscrng2  13647  ringpropd  13670  ringinvnz1ne0  13681  mulgass2  13690  ring1  13691  imasring  13696  opprnegg  13715  dvdsrd  13726  dvreq1  13774  rhmmul  13796  isrhm2d  13797  rhmopp  13808  rhmunitinv  13810  islring  13824  rrgval  13894  unitrrg  13899  opprdomnbg  13906  islmod  13923  lmodlema  13924  islmodd  13925  lmodvsmmulgdi  13955  lmodprop2d  13980  rmodislmodlem  13982  rmodislmod  13983  rnglidlmsgrp  14129  rnglidlrng  14130  quscrng  14165  cnfldmulg  14208  cnfldexp  14209  gsumfzfsumlemm  14219  zndvds  14281  znf1o  14283  znunit  14291  psr1clfi  14316  txcnp  14591  cnmpt11  14603  cnmpt21  14611  cnmptcom  14618  isxms  14771  xmspropd  14797  bdmopn  14824  dvexp  15031  dvmptfsum  15045  rpcxpmul2  15233  wilthlem1  15300  mpodvdsmulf1o  15310  fsumdvdsmul  15311  perfect  15321  lgsne0  15363  gausslemma2d  15394  lgseisenlem2  15396  lgsquad2lem2  15407  2lgslem1a  15413  2lgslem1b  15414  nninffeq  15751