Theorem eqeq12d 2244

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  cdeqeq  3023  sbceqg  3140  csbing  3411  uniprg  3903  unisng  3905  intprg  3956  iununir  4049  csbopabg  4162  undifexmid  4278  exmidundif  4291  exmidundifim  4292  limeq  4469  onsucuni2  4657  ordpwsucexmid  4663  csbima12g  5092  dmsnsnsng  5209  cnvsng  5217  csbiotag  5314  fvmptf  5732  eqfnfv2f  5741  fvreseq  5743  fmptco  5806  fnressn  5832  fvsng  5842  cocan1  5920  cocan2  5921  fliftfun  5929  csbriotag  5977  oveqrspc2v  6037  csbov123g  6049  eqfnov  6120  ovmpos  6137  ov2gf  6138  ovmpodxf  6139  caovcomg  6170  caovassg  6173  caovcang  6176  caovcanrd  6178  caovcan  6179  caovdig  6189  caovdirg  6192  caovimo  6208  offveqb  6247  caofid0l  6254  caofid0r  6255  op1stg  6305  op2ndg  6306  f1o2ndf1  6385  tfrlem1  6465  tfrlem3ag  6466  tfrlem3a  6467  tfrlem5  6471  tfrlem9  6476  tfr0dm  6479  tfrlemiubacc  6487  tfrlemiex  6488  tfrlemi1  6489  tfr1onlem3ag  6494  tfr1onlemubacc  6503  tfr1onlemex  6504  tfr1onlemaccex  6505  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllemubacc  6516  tfrcllemex  6517  tfrcllemaccex  6518  tfrcllemres  6519  tfrcldm  6520  tfri3  6524  rdg0g  6545  frecrdg  6565  nna0r  6637  nnacom  6643  nnaass  6644  nndi  6645  nnmass  6646  nnmsucr  6647  nnmcom  6648  ecopovtrn  6792  ecopovsymg  6794  ecopovtrng  6795  ecovcom  6802  ecovicom  6803  ecovass  6804  ecoviass  6805  ecovdi  6806  ecovidi  6807  dom2lem  6936  ordiso2  7218  inl11  7248  updjud  7265  omp1eomlem  7277  difinfsnlem  7282  nnnninfeq  7311  nninfwlporlemd  7355  nninfwlpor  7357  nninfinfwlpo  7363  exmidfodomrlemrALT  7397  exmidaclem  7406  addcanpig  7537  mulcanpig  7538  mulcmpblnq  7571  mulpipqqs  7576  ordpipqqs  7577  mulidnq  7592  enq0sym  7635  nqnq0  7644  mulcmpblnq0  7647  distrnq0  7662  mulcomnq0  7663  addassnq0  7665  nq02m  7668  genipv  7712  cauappcvgprlemladd  7861  addcmpblnr  7942  0idsr  7970  1idsr  7971  axaddcom  8073  ax1rid  8080  ax0id  8081  rereceu  8092  axcaucvg  8103  mulrid  8159  readdcan  8302  cnegexlem1  8337  cnegexlem3  8339  addcan  8342  addcan2  8343  apti  8785  mulcanapd  8824  mulcanap2d  8825  div11ap  8863  divmuleqap  8880  conjmulap  8892  eqneg  8895  cnref1o  9863  fzsuc2  10292  fzprval  10295  fztpval  10296  qtri3or  10477  modqadd1  10600  modqmul1  10616  addmodlteq  10637  frec2uzrdg  10648  frecuzrdgg  10655  seq3val  10699  seqvalcd  10700  seq3fveq2  10714  seqfveq2g  10716  seqfveqg  10717  seq3fveq  10718  seq3feq  10719  seq3shft2  10720  seqshft2g  10721  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seqcaopr3g  10731  seq3caopr2  10732  seqcaopr2g  10733  iseqf1olemkle  10736  iseqf1olemklt  10737  iseqf1olemqk  10746  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1olemp  10754  seq3f1oleml  10755  seqf1oglem2a  10757  seqf1oglem2  10759  seqf1og  10760  seq3id  10764  seq3id2  10765  seq3homo  10766  seqhomog  10769  seqfeq4g  10770  mulexp  10817  expadd  10820  expmul  10823  modqexp  10905  nn0opth2d  10962  bcpasc  11005  hashennn  11019  hashen  11023  omgadd  11041  hashfzo  11062  hashfzp1  11064  hashxp  11066  hashfacen  11076  seq3coll  11082  eqs1  11181  swrdspsleq  11220  pfxeq  11249  pfxsuff1eqwrdeq  11252  ccatopth2  11270  cats1un  11274  swrdccatin1  11278  swrdccat3blem  11292  shftvalg  11368  shftval4g  11369  replim  11391  cjreb  11398  cjexp  11425  absexp  11611  recan  11641  minclpr  11769  mingeb  11774  sumeq2  11891  zsumdc  11916  fsum3  11919  fsumf1o  11922  fsum3cvg2  11926  fsumadd  11938  isummulc2  11958  fsum2d  11967  fsummulc2  11980  fsumconst  11986  modfsummod  11990  fsumparts  12002  fsumrelem  12003  fsumiun  12009  binom  12016  bcxmas  12021  isumshft  12022  isumnn0nn  12025  mertenslem2  12068  clim2prod  12071  prodfrecap  12078  prodeq2  12089  zproddc  12111  fprodseq  12115  fprodf1o  12120  prodsnf  12124  fprodfac  12147  fprodabs  12148  fprodconst  12152  fprod2d  12155  fprodrec  12161  fprodmodd  12173  efne0  12210  efexp  12214  demoivreALT  12306  moddvds  12331  bitsinv1  12494  gcddiv  12561  alginv  12590  algfx  12595  lcmneg  12617  lcmid  12623  lcmgcdeq  12626  divgcdcoprm0  12644  cncongr1  12646  cncongr2  12647  nn0gcdsq  12743  crth  12767  eulerthlema  12773  eulerthlemh  12774  pythagtriplem1  12809  pcqmul  12847  pcexp  12853  pcneg  12869  pcmpt  12887  pcfac  12894  1arith  12911  setscomd  13094  ercpbllemg  13384  mgmidmo  13426  mgmlrid  13433  lidrideqd  13435  lidrididd  13436  grpinvalem  13439  grpinva  13440  issgrp  13457  isnsgrp  13460  sgrpass  13462  sgrp1  13465  issgrpd  13466  sgrppropd  13467  ismndd  13491  mndpropd  13494  imasmnd2  13506  mnd1  13509  mnd1id  13510  ismhm  13515  mhmpropd  13520  mhmlin  13521  mhmeql  13546  isgrp  13560  grppropd  13571  isgrpd2e  13574  dfgrp2  13581  isgrpid2  13594  grpidd2  13595  grpinvfvalg  13596  grpinvpropdg  13629  grpidssd  13630  grpinvssd  13631  grpsubrcan  13635  dfgrp3mlem  13652  grplactcnv  13656  imasgrp2  13668  mhmlem  13672  mulgnn0p1  13691  mulgaddcom  13704  mulginvcom  13705  mulgneg2  13714  mulgnnass  13715  mulgnn0ass  13716  mulgass  13717  mhmmulg  13721  isghm  13801  ghmlin  13806  ghmeql  13825  iscmn  13851  cmnpropd  13853  iscmnd  13856  abladdsub4  13872  imasabl  13894  gsumfzconst  13899  isrng  13918  rngass  13923  rngdi  13924  rngdir  13925  rngpropd  13939  imasrng  13940  issrg  13949  srgmulgass  13973  srgpcomp  13974  srg1expzeq1  13979  isring  13984  iscrng2  13999  ringpropd  14022  ringinvnz1ne0  14033  mulgass2  14042  ring1  14043  imasring  14048  opprnegg  14067  dvdsrd  14079  dvreq1  14127  rhmmul  14149  isrhm2d  14150  rhmopp  14161  rhmunitinv  14163  islring  14177  rrgval  14247  unitrrg  14252  opprdomnbg  14259  islmod  14276  lmodlema  14277  islmodd  14278  lmodvsmmulgdi  14308  lmodprop2d  14333  rmodislmodlem  14335  rmodislmod  14336  rnglidlmsgrp  14482  rnglidlrng  14483  quscrng  14518  cnfldmulg  14561  cnfldexp  14562  gsumfzfsumlemm  14572  zndvds  14634  znf1o  14636  znunit  14644  psr1clfi  14673  txcnp  14966  cnmpt11  14978  cnmpt21  14986  cnmptcom  14993  isxms  15146  xmspropd  15172  bdmopn  15199  dvexp  15406  dvmptfsum  15420  rpcxpmul2  15608  wilthlem1  15675  mpodvdsmulf1o  15685  fsumdvdsmul  15686  perfect  15696  lgsne0  15738  gausslemma2d  15769  lgseisenlem2  15771  lgsquad2lem2  15782  2lgslem1a  15788  2lgslem1b  15789  usgredg2v  16043  wkslem1  16092  wkslem2  16093  iswlk  16095  uspgr2wlkeq  16137  2wlklem  16146  wlkres  16149  nninffeq  16500