Theorem eqeq12d 2253

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3950  unisng  3952  intprg  4003  iununir  4096  csbopabg  4210  undifexmid  4332  exmidundif  4345  exmidundifim  4346  limeq  4524  onsucuni2  4713  ordpwsucexmid  4719  csbima12g  5151  dmsnsnsng  5268  cnvsng  5276  csbiotag  5373  fvmptf  5801  eqfnfv2f  5813  fvreseq  5815  fmptco  5877  fnressn  5904  fvsng  5914  cocan1  5996  cocan2  5997  fliftfun  6005  csbriotag  6055  oveqrspc2v  6115  csbov123g  6127  eqfnov  6198  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  caovcomg  6248  caovassg  6251  caovcang  6254  caovcanrd  6256  caovcan  6257  caovdig  6267  caovdirg  6270  caovimo  6286  offveqb  6326  caofid0l  6333  caofid0r  6334  op1stg  6388  op2ndg  6389  f1o2ndf1  6468  tfrlem1  6583  tfrlem3ag  6584  tfrlem3a  6585  tfrlem5  6589  tfrlem9  6594  tfr0dm  6597  tfrlemiubacc  6605  tfrlemiex  6606  tfrlemi1  6607  tfr1onlem3ag  6612  tfr1onlemubacc  6621  tfr1onlemex  6622  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemubacc  6634  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  tfri3  6642  rdg0g  6663  frecrdg  6683  nna0r  6755  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  ecopovtrn  6910  ecopovsymg  6912  ecopovtrng  6913  ecovcom  6920  ecovicom  6921  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  dom2lem  7063  ordiso2  7382  inl11  7412  updjud  7429  omp1eomlem  7441  difinfsnlem  7446  nnnninfeq  7475  nninfwlporlemd  7519  nninfwlpor  7521  nninfinfwlpo  7527  exmidfodomrlemrALT  7562  exmidaclem  7571  addcanpig  7708  mulcanpig  7709  mulcmpblnq  7742  mulpipqqs  7747  ordpipqqs  7748  mulidnq  7763  enq0sym  7806  nqnq0  7815  mulcmpblnq0  7818  distrnq0  7833  mulcomnq0  7834  addassnq0  7836  nq02m  7839  genipv  7883  cauappcvgprlemladd  8032  addcmpblnr  8113  0idsr  8141  1idsr  8142  axaddcom  8244  ax1rid  8251  ax0id  8252  rereceu  8263  axcaucvg  8274  mulrid  8330  readdcan  8474  cnegexlem1  8509  cnegexlem3  8511  addcan  8514  addcan2  8515  apti  8959  mulcanapd  8998  mulcanap2d  8999  div11ap  9039  divmuleqap  9056  conjmulap  9068  eqneg  9071  ofsubeq0  9301  cnref1o  10069  fzsuc2  10504  fzprval  10507  fztpval  10508  qtri3or  10693  modqadd1  10820  modqmul1  10836  addmodlteq  10857  frec2uzrdg  10868  frecuzrdgg  10875  seq3val  10919  seqvalcd  10920  seq3fveq2  10934  seqfveq2g  10936  seqfveqg  10937  seq3fveq  10938  seq3feq  10939  seq3shft2  10940  seqshft2g  10941  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  seqcaopr3g  10951  seq3caopr2  10952  seqcaopr2g  10953  iseqf1olemkle  10956  iseqf1olemklt  10957  iseqf1olemqk  10966  seq3f1olemqsum  10972  seq3f1olemstep  10973  seq3f1olemp  10974  seq3f1oleml  10975  seqf1oglem2a  10977  seqf1oglem2  10979  seqf1og  10980  seq3id  10984  seq3id2  10985  seq3homo  10986  seqhomog  10989  seqfeq4g  10990  mulexp  11037  expadd  11040  expmul  11043  modqexp  11126  nn0opth2d  11184  bcpasc  11227  bcm1n  11230  hashennn  11242  hashen  11246  omgadd  11265  hashfzo  11286  hashfzp1  11288  hashxp  11290  hashmap  11291  hashfibclem  11305  hashfibc  11306  hashfacen  11307  hashf1lem1  11308  hashf1lem2  11309  hashf1  11310  seq3coll  11317  eqs1  11419  swrdspsleq  11462  pfxeq  11491  pfxsuff1eqwrdeq  11494  ccatopth2  11512  cats1un  11516  swrdccatin1  11520  swrdccat3blem  11534  shftvalg  11624  shftval4g  11625  replim  11647  cjreb  11654  cjexp  11681  absexp  11869  recan  11899  minclpr  12028  mingeb  12034  sumeq2  12151  zsumdc  12177  fsum3  12180  fsumf1o  12183  fsum3cvg2  12187  fsumadd  12199  isummulc2  12219  fsum2d  12228  fsummulc2  12241  fsumconst  12247  modfsummod  12251  fsumparts  12263  fsumrelem  12264  fsumiun  12270  binom  12277  bcxmas  12282  isumshft  12283  isumnn0nn  12286  mertenslem2  12329  clim2prod  12332  prodfrecap  12339  prodeq2  12350  zproddc  12372  fprodseq  12376  fprodf1o  12381  prodsnf  12385  fprodfac  12408  fprodabs  12409  fprodconst  12413  fprod2d  12416  fprodrec  12422  fprodmodd  12434  efne0  12471  efexp  12475  demoivreALT  12567  moddvds  12592  bitsinv1  12755  gcddiv  12822  alginv  12851  algfx  12856  lcmneg  12878  lcmid  12884  lcmgcdeq  12887  divgcdcoprm0  12905  cncongr1  12907  cncongr2  12908  nn0gcdsq  13006  crth  13032  eulerthlema  13038  eulerthlemh  13039  pythagtriplem1  13074  pcqmul  13112  pcexp  13118  pcneg  13134  pcmpt  13152  pcfac  13159  1arith  13176  setscomd  13452  ercpbllemg  13711  mgmidmo  13752  mgmlrid  13759  lidrideqd  13761  lidrididd  13762  grpinvalem  13765  grpinva  13766  issgrp  13778  isnsgrp  13781  sgrpass  13783  sgrp1  13786  issgrpd  13787  sgrppropd  13788  ismndd  13810  mndpropd  13813  imasmnd2  13819  mnd1  13822  mnd1id  13823  ismhm  13828  mhmpropd  13833  mhmlin  13834  mhmeql  13859  isgrp  13871  grppropd  13882  isgrpd2e  13885  dfgrp2  13892  isgrpid2  13905  grpidd2  13906  grpinvfvalg  13907  grpinvpropdg  13940  grpidssd  13941  grpinvssd  13942  grpsubrcan  13946  dfgrp3mlem  13963  grplactcnv  13967  imasgrp2  13973  mhmlem  13977  mulgnn0p1  13996  mulgaddcom  14009  mulginvcom  14010  mulgneg2  14019  mulgnnass  14020  mulgnn0ass  14021  mulgass  14022  mhmmulg  14026  isghm  14106  ghmlin  14111  ghmeql  14130  cntzex  14151  cntzfval  14153  elcntz  14155  cntzsnval  14157  elcntzsn  14158  cntzi  14163  resscntz  14167  cntzmhm  14174  iscmn  14187  cmnpropd  14189  iscmnd  14192  cmnsubm  14203  abladdsub4  14209  imasabl  14231  gzsumconst  14234  gsummptfidmadd  14252  gsummptfidmsplit  14255  gsumresfi  14264  gsumconstcmn  14267  gsum2dfilem2  14273  isrng  14341  rngass  14346  rngdi  14347  rngdir  14348  rngpropd  14362  imasrng  14363  issrg  14377  srgmulgass  14401  srgpcomp  14402  srg1expzeq1  14407  isring  14412  iscrng2  14427  ringpropd  14451  ringinvnz1ne0  14462  mulgass2  14471  ring1  14472  imasring  14479  opprnegg  14499  dvdsrd  14511  dvreq1  14559  rhmmul  14581  isrhm2d  14582  rhmopp  14593  rhmunitinv  14595  islring  14609  opprlring  14614  rrgval  14680  unitrrg  14686  opprdomnbg  14693  islmod  14737  lmodlema  14738  islmodd  14739  lmodvsmmulgdi  14770  lmodprop2d  14795  rmodislmodlem  14797  rmodislmod  14798  rnglidlmsgrp  14944  rnglidlrng  14945  quscrng  14980  cnfldmulg  15023  cnfldexp  15024  gsumfsum  15033  zndvds  15094  znf1o  15096  znunit  15104  isassa  15112  assalem  15113  isassad  15121  assapropd  15124  assamulgscm  15153  psr1clfi  15203  mvrf1fi  15215  txcnp  15509  cnmpt11  15521  cnmpt21  15529  cnmptcom  15536  isxms  15689  xmspropd  15715  bdmopn  15742  dvexp  15949  dvmptfsum  15963  sineq0re  16088  rpcxpmul2  16158  wilthlem1  16244  mpodvdsmulf1o  16296  fsumdvdsmul  16297  perfect  16313  lgsne0  16374  gausslemma2d  16405  lgseisenlem2  16407  lgsquad2lem2  16418  2lgslem1a  16424  2lgslem1b  16425  usgredg2v  16682  issubgr  16715  wkslem1  16778  wkslem2  16779  iswlk  16781  uspgr2wlkeq  16823  2wlklem  16834  wlkres  16837  eupth2lem3fi  16934  eupth2fi  16937  depindlem1  16964  depindlem2  16965  depindlem3  16966  depind  16967  nninffeq  17281