Theorem eqeq12d 2246

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  cdeqeq  3026  sbceqg  3143  csbing  3414  uniprg  3908  unisng  3910  intprg  3961  iununir  4054  csbopabg  4167  undifexmid  4283  exmidundif  4296  exmidundifim  4297  limeq  4474  onsucuni2  4662  ordpwsucexmid  4668  csbima12g  5097  dmsnsnsng  5214  cnvsng  5222  csbiotag  5319  fvmptf  5739  eqfnfv2f  5748  fvreseq  5750  fmptco  5813  fnressn  5840  fvsng  5850  cocan1  5928  cocan2  5929  fliftfun  5937  csbriotag  5985  oveqrspc2v  6045  csbov123g  6057  eqfnov  6128  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  caovcomg  6178  caovassg  6181  caovcang  6184  caovcanrd  6186  caovcan  6187  caovdig  6197  caovdirg  6200  caovimo  6216  offveqb  6255  caofid0l  6262  caofid0r  6263  op1stg  6313  op2ndg  6314  f1o2ndf1  6393  tfrlem1  6474  tfrlem3ag  6475  tfrlem3a  6476  tfrlem5  6480  tfrlem9  6485  tfr0dm  6488  tfrlemiubacc  6496  tfrlemiex  6497  tfrlemi1  6498  tfr1onlem3ag  6503  tfr1onlemubacc  6512  tfr1onlemex  6513  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemubacc  6525  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  tfri3  6533  rdg0g  6554  frecrdg  6574  nna0r  6646  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  ecopovtrn  6801  ecopovsymg  6803  ecopovtrng  6804  ecovcom  6811  ecovicom  6812  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  dom2lem  6945  ordiso2  7234  inl11  7264  updjud  7281  omp1eomlem  7293  difinfsnlem  7298  nnnninfeq  7327  nninfwlporlemd  7371  nninfwlpor  7373  nninfinfwlpo  7379  exmidfodomrlemrALT  7414  exmidaclem  7423  addcanpig  7554  mulcanpig  7555  mulcmpblnq  7588  mulpipqqs  7593  ordpipqqs  7594  mulidnq  7609  enq0sym  7652  nqnq0  7661  mulcmpblnq0  7664  distrnq0  7679  mulcomnq0  7680  addassnq0  7682  nq02m  7685  genipv  7729  cauappcvgprlemladd  7878  addcmpblnr  7959  0idsr  7987  1idsr  7988  axaddcom  8090  ax1rid  8097  ax0id  8098  rereceu  8109  axcaucvg  8120  mulrid  8176  readdcan  8319  cnegexlem1  8354  cnegexlem3  8356  addcan  8359  addcan2  8360  apti  8802  mulcanapd  8841  mulcanap2d  8842  div11ap  8880  divmuleqap  8897  conjmulap  8909  eqneg  8912  cnref1o  9885  fzsuc2  10314  fzprval  10317  fztpval  10318  qtri3or  10501  modqadd1  10624  modqmul1  10640  addmodlteq  10661  frec2uzrdg  10672  frecuzrdgg  10679  seq3val  10723  seqvalcd  10724  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqk  10770  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem2a  10781  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3id2  10789  seq3homo  10790  seqhomog  10793  seqfeq4g  10794  mulexp  10841  expadd  10844  expmul  10847  modqexp  10929  nn0opth2d  10986  bcpasc  11029  hashennn  11043  hashen  11047  omgadd  11066  hashfzo  11087  hashfzp1  11089  hashxp  11091  hashfacen  11101  seq3coll  11107  eqs1  11209  swrdspsleq  11252  pfxeq  11281  pfxsuff1eqwrdeq  11284  ccatopth2  11302  cats1un  11306  swrdccatin1  11310  swrdccat3blem  11324  shftvalg  11401  shftval4g  11402  replim  11424  cjreb  11431  cjexp  11458  absexp  11644  recan  11674  minclpr  11802  mingeb  11807  sumeq2  11924  zsumdc  11950  fsum3  11953  fsumf1o  11956  fsum3cvg2  11960  fsumadd  11972  isummulc2  11992  fsum2d  12001  fsummulc2  12014  fsumconst  12020  modfsummod  12024  fsumparts  12036  fsumrelem  12037  fsumiun  12043  binom  12050  bcxmas  12055  isumshft  12056  isumnn0nn  12059  mertenslem2  12102  clim2prod  12105  prodfrecap  12112  prodeq2  12123  zproddc  12145  fprodseq  12149  fprodf1o  12154  prodsnf  12158  fprodfac  12181  fprodabs  12182  fprodconst  12186  fprod2d  12189  fprodrec  12195  fprodmodd  12207  efne0  12244  efexp  12248  demoivreALT  12340  moddvds  12365  bitsinv1  12528  gcddiv  12595  alginv  12624  algfx  12629  lcmneg  12651  lcmid  12657  lcmgcdeq  12660  divgcdcoprm0  12678  cncongr1  12680  cncongr2  12681  nn0gcdsq  12777  crth  12801  eulerthlema  12807  eulerthlemh  12808  pythagtriplem1  12843  pcqmul  12881  pcexp  12887  pcneg  12903  pcmpt  12921  pcfac  12928  1arith  12945  setscomd  13128  ercpbllemg  13418  mgmidmo  13460  mgmlrid  13467  lidrideqd  13469  lidrididd  13470  grpinvalem  13473  grpinva  13474  issgrp  13491  isnsgrp  13494  sgrpass  13496  sgrp1  13499  issgrpd  13500  sgrppropd  13501  ismndd  13525  mndpropd  13528  imasmnd2  13540  mnd1  13543  mnd1id  13544  ismhm  13549  mhmpropd  13554  mhmlin  13555  mhmeql  13580  isgrp  13594  grppropd  13605  isgrpd2e  13608  dfgrp2  13615  isgrpid2  13628  grpidd2  13629  grpinvfvalg  13630  grpinvpropdg  13663  grpidssd  13664  grpinvssd  13665  grpsubrcan  13669  dfgrp3mlem  13686  grplactcnv  13690  imasgrp2  13702  mhmlem  13706  mulgnn0p1  13725  mulgaddcom  13738  mulginvcom  13739  mulgneg2  13748  mulgnnass  13749  mulgnn0ass  13750  mulgass  13751  mhmmulg  13755  isghm  13835  ghmlin  13840  ghmeql  13859  iscmn  13885  cmnpropd  13887  iscmnd  13890  abladdsub4  13906  imasabl  13928  gsumfzconst  13933  isrng  13953  rngass  13958  rngdi  13959  rngdir  13960  rngpropd  13974  imasrng  13975  issrg  13984  srgmulgass  14008  srgpcomp  14009  srg1expzeq1  14014  isring  14019  iscrng2  14034  ringpropd  14057  ringinvnz1ne0  14068  mulgass2  14077  ring1  14078  imasring  14083  opprnegg  14102  dvdsrd  14114  dvreq1  14162  rhmmul  14184  isrhm2d  14185  rhmopp  14196  rhmunitinv  14198  islring  14212  rrgval  14282  unitrrg  14287  opprdomnbg  14294  islmod  14311  lmodlema  14312  islmodd  14313  lmodvsmmulgdi  14343  lmodprop2d  14368  rmodislmodlem  14370  rmodislmod  14371  rnglidlmsgrp  14517  rnglidlrng  14518  quscrng  14553  cnfldmulg  14596  cnfldexp  14597  gsumfzfsumlemm  14607  zndvds  14669  znf1o  14671  znunit  14679  psr1clfi  14708  txcnp  15001  cnmpt11  15013  cnmpt21  15021  cnmptcom  15028  isxms  15181  xmspropd  15207  bdmopn  15234  dvexp  15441  dvmptfsum  15455  rpcxpmul2  15643  wilthlem1  15710  mpodvdsmulf1o  15720  fsumdvdsmul  15721  perfect  15731  lgsne0  15773  gausslemma2d  15804  lgseisenlem2  15806  lgsquad2lem2  15817  2lgslem1a  15823  2lgslem1b  15824  usgredg2v  16081  issubgr  16114  wkslem1  16177  wkslem2  16178  iswlk  16180  uspgr2wlkeq  16222  2wlklem  16233  wlkres  16236  eupth2lem3fi  16333  eupth2fi  16336  depindlem1  16351  depindlem2  16352  depindlem3  16353  depind  16354  nninffeq  16648