Theorem eqeq12d 2247

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  cdeqeq  3036  sbceqg  3153  csbing  3427  uniprg  3928  unisng  3930  intprg  3981  iununir  4074  csbopabg  4187  undifexmid  4305  exmidundif  4318  exmidundifim  4319  limeq  4497  onsucuni2  4685  ordpwsucexmid  4691  csbima12g  5122  dmsnsnsng  5239  cnvsng  5247  csbiotag  5344  fvmptf  5769  eqfnfv2f  5778  fvreseq  5780  fmptco  5842  fnressn  5869  fvsng  5879  cocan1  5959  cocan2  5960  fliftfun  5968  csbriotag  6016  oveqrspc2v  6076  csbov123g  6088  eqfnov  6159  ovmpos  6176  ov2gf  6177  ovmpodxf  6178  caovcomg  6209  caovassg  6212  caovcang  6215  caovcanrd  6217  caovcan  6218  caovdig  6228  caovdirg  6231  caovimo  6247  offveqb  6285  caofid0l  6292  caofid0r  6293  op1stg  6343  op2ndg  6344  f1o2ndf1  6423  tfrlem1  6538  tfrlem3ag  6539  tfrlem3a  6540  tfrlem5  6544  tfrlem9  6549  tfr0dm  6552  tfrlemiubacc  6560  tfrlemiex  6561  tfrlemi1  6562  tfr1onlem3ag  6567  tfr1onlemubacc  6576  tfr1onlemex  6577  tfr1onlemaccex  6578  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllemubacc  6589  tfrcllemex  6590  tfrcllemaccex  6591  tfrcllemres  6592  tfrcldm  6593  tfri3  6597  rdg0g  6618  frecrdg  6638  nna0r  6710  nnacom  6716  nnaass  6717  nndi  6718  nnmass  6719  nnmsucr  6720  nnmcom  6721  ecopovtrn  6865  ecopovsymg  6867  ecopovtrng  6868  ecovcom  6875  ecovicom  6876  ecovass  6877  ecoviass  6878  ecovdi  6879  ecovidi  6880  dom2lem  7010  ordiso2  7325  inl11  7355  updjud  7372  omp1eomlem  7384  difinfsnlem  7389  nnnninfeq  7418  nninfwlporlemd  7462  nninfwlpor  7464  nninfinfwlpo  7470  exmidfodomrlemrALT  7505  exmidaclem  7514  addcanpig  7648  mulcanpig  7649  mulcmpblnq  7682  mulpipqqs  7687  ordpipqqs  7688  mulidnq  7703  enq0sym  7746  nqnq0  7755  mulcmpblnq0  7758  distrnq0  7773  mulcomnq0  7774  addassnq0  7776  nq02m  7779  genipv  7823  cauappcvgprlemladd  7972  addcmpblnr  8053  0idsr  8081  1idsr  8082  axaddcom  8184  ax1rid  8191  ax0id  8192  rereceu  8203  axcaucvg  8214  mulrid  8270  readdcan  8412  cnegexlem1  8447  cnegexlem3  8449  addcan  8452  addcan2  8453  apti  8895  mulcanapd  8934  mulcanap2d  8935  div11ap  8973  divmuleqap  8990  conjmulap  9002  eqneg  9005  cnref1o  9982  fzsuc2  10412  fzprval  10415  fztpval  10416  qtri3or  10599  modqadd1  10722  modqmul1  10738  addmodlteq  10759  frec2uzrdg  10770  frecuzrdgg  10777  seq3val  10821  seqvalcd  10822  seq3fveq2  10836  seqfveq2g  10838  seqfveqg  10839  seq3fveq  10840  seq3feq  10841  seq3shft2  10842  seqshft2g  10843  seq3split  10849  seqsplitg  10850  seq3caopr3  10852  seqcaopr3g  10853  seq3caopr2  10854  seqcaopr2g  10855  iseqf1olemkle  10858  iseqf1olemklt  10859  iseqf1olemqk  10868  seq3f1olemqsum  10874  seq3f1olemstep  10875  seq3f1olemp  10876  seq3f1oleml  10877  seqf1oglem2a  10879  seqf1oglem2  10881  seqf1og  10882  seq3id  10886  seq3id2  10887  seq3homo  10888  seqhomog  10891  seqfeq4g  10892  mulexp  10939  expadd  10942  expmul  10945  modqexp  11027  nn0opth2d  11084  bcpasc  11127  hashennn  11141  hashen  11145  omgadd  11164  hashfzo  11185  hashfzp1  11187  hashxp  11189  hashfibclem  11202  hashfibc  11203  hashfacen  11204  seq3coll  11210  eqs1  11312  swrdspsleq  11355  pfxeq  11384  pfxsuff1eqwrdeq  11387  ccatopth2  11405  cats1un  11409  swrdccatin1  11413  swrdccat3blem  11427  shftvalg  11517  shftval4g  11518  replim  11540  cjreb  11547  cjexp  11574  absexp  11760  recan  11790  minclpr  11918  mingeb  11923  sumeq2  12040  zsumdc  12066  fsum3  12069  fsumf1o  12072  fsum3cvg2  12076  fsumadd  12088  isummulc2  12108  fsum2d  12117  fsummulc2  12130  fsumconst  12136  modfsummod  12140  fsumparts  12152  fsumrelem  12153  fsumiun  12159  binom  12166  bcxmas  12171  isumshft  12172  isumnn0nn  12175  mertenslem2  12218  clim2prod  12221  prodfrecap  12228  prodeq2  12239  zproddc  12261  fprodseq  12265  fprodf1o  12270  prodsnf  12274  fprodfac  12297  fprodabs  12298  fprodconst  12302  fprod2d  12305  fprodrec  12311  fprodmodd  12323  efne0  12360  efexp  12364  demoivreALT  12456  moddvds  12481  bitsinv1  12644  gcddiv  12711  alginv  12740  algfx  12745  lcmneg  12767  lcmid  12773  lcmgcdeq  12776  divgcdcoprm0  12794  cncongr1  12796  cncongr2  12797  nn0gcdsq  12893  crth  12917  eulerthlema  12923  eulerthlemh  12924  pythagtriplem1  12959  pcqmul  12997  pcexp  13003  pcneg  13019  pcmpt  13037  pcfac  13044  1arith  13061  setscomd  13245  ercpbllemg  13535  mgmidmo  13577  mgmlrid  13584  lidrideqd  13586  lidrididd  13587  grpinvalem  13590  grpinva  13591  issgrp  13608  isnsgrp  13611  sgrpass  13613  sgrp1  13616  issgrpd  13617  sgrppropd  13618  ismndd  13642  mndpropd  13645  imasmnd2  13657  mnd1  13660  mnd1id  13661  ismhm  13666  mhmpropd  13671  mhmlin  13672  mhmeql  13697  isgrp  13711  grppropd  13722  isgrpd2e  13725  dfgrp2  13732  isgrpid2  13745  grpidd2  13746  grpinvfvalg  13747  grpinvpropdg  13780  grpidssd  13781  grpinvssd  13782  grpsubrcan  13786  dfgrp3mlem  13803  grplactcnv  13807  imasgrp2  13819  mhmlem  13823  mulgnn0p1  13842  mulgaddcom  13855  mulginvcom  13856  mulgneg2  13865  mulgnnass  13866  mulgnn0ass  13867  mulgass  13868  mhmmulg  13872  isghm  13952  ghmlin  13957  ghmeql  13976  iscmn  14002  cmnpropd  14004  iscmnd  14007  abladdsub4  14023  imasabl  14045  gsumfzconst  14050  isrng  14070  rngass  14075  rngdi  14076  rngdir  14077  rngpropd  14091  imasrng  14092  issrg  14101  srgmulgass  14125  srgpcomp  14126  srg1expzeq1  14131  isring  14136  iscrng2  14151  ringpropd  14174  ringinvnz1ne0  14185  mulgass2  14194  ring1  14195  imasring  14200  opprnegg  14219  dvdsrd  14231  dvreq1  14279  rhmmul  14301  isrhm2d  14302  rhmopp  14313  rhmunitinv  14315  islring  14329  rrgval  14399  unitrrg  14405  opprdomnbg  14412  islmod  14431  lmodlema  14432  islmodd  14433  lmodvsmmulgdi  14463  lmodprop2d  14488  rmodislmodlem  14490  rmodislmod  14491  rnglidlmsgrp  14637  rnglidlrng  14638  quscrng  14673  cnfldmulg  14716  cnfldexp  14717  gsumfzfsumlemm  14727  zndvds  14789  znf1o  14791  znunit  14799  psr1clfi  14835  txcnp  15128  cnmpt11  15140  cnmpt21  15148  cnmptcom  15155  isxms  15308  xmspropd  15334  bdmopn  15361  dvexp  15568  dvmptfsum  15582  rpcxpmul2  15770  wilthlem1  15840  mpodvdsmulf1o  15850  fsumdvdsmul  15851  perfect  15861  lgsne0  15903  gausslemma2d  15934  lgseisenlem2  15936  lgsquad2lem2  15947  2lgslem1a  15953  2lgslem1b  15954  usgredg2v  16211  issubgr  16244  wkslem1  16307  wkslem2  16308  iswlk  16310  uspgr2wlkeq  16352  2wlklem  16363  wlkres  16366  eupth2lem3fi  16463  eupth2fi  16466  depindlem1  16493  depindlem2  16494  depindlem3  16495  depind  16496  nninffeq  16790