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  3024  sbceqg  3141  csbing  3412  uniprg  3906  unisng  3908  intprg  3959  iununir  4052  csbopabg  4165  undifexmid  4281  exmidundif  4294  exmidundifim  4295  limeq  4472  onsucuni2  4660  ordpwsucexmid  4666  csbima12g  5095  dmsnsnsng  5212  cnvsng  5220  csbiotag  5317  fvmptf  5735  eqfnfv2f  5744  fvreseq  5746  fmptco  5809  fnressn  5835  fvsng  5845  cocan1  5923  cocan2  5924  fliftfun  5932  csbriotag  5980  oveqrspc2v  6040  csbov123g  6052  eqfnov  6123  ovmpos  6140  ov2gf  6141  ovmpodxf  6142  caovcomg  6173  caovassg  6176  caovcang  6179  caovcanrd  6181  caovcan  6182  caovdig  6192  caovdirg  6195  caovimo  6211  offveqb  6250  caofid0l  6257  caofid0r  6258  op1stg  6308  op2ndg  6309  f1o2ndf1  6388  tfrlem1  6469  tfrlem3ag  6470  tfrlem3a  6471  tfrlem5  6475  tfrlem9  6480  tfr0dm  6483  tfrlemiubacc  6491  tfrlemiex  6492  tfrlemi1  6493  tfr1onlem3ag  6498  tfr1onlemubacc  6507  tfr1onlemex  6508  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemubacc  6520  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  tfri3  6528  rdg0g  6549  frecrdg  6569  nna0r  6641  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  dom2lem  6940  ordiso2  7228  inl11  7258  updjud  7275  omp1eomlem  7287  difinfsnlem  7292  nnnninfeq  7321  nninfwlporlemd  7365  nninfwlpor  7367  nninfinfwlpo  7373  exmidfodomrlemrALT  7407  exmidaclem  7416  addcanpig  7547  mulcanpig  7548  mulcmpblnq  7581  mulpipqqs  7586  ordpipqqs  7587  mulidnq  7602  enq0sym  7645  nqnq0  7654  mulcmpblnq0  7657  distrnq0  7672  mulcomnq0  7673  addassnq0  7675  nq02m  7678  genipv  7722  cauappcvgprlemladd  7871  addcmpblnr  7952  0idsr  7980  1idsr  7981  axaddcom  8083  ax1rid  8090  ax0id  8091  rereceu  8102  axcaucvg  8113  mulrid  8169  readdcan  8312  cnegexlem1  8347  cnegexlem3  8349  addcan  8352  addcan2  8353  apti  8795  mulcanapd  8834  mulcanap2d  8835  div11ap  8873  divmuleqap  8890  conjmulap  8902  eqneg  8905  cnref1o  9878  fzsuc2  10307  fzprval  10310  fztpval  10311  qtri3or  10493  modqadd1  10616  modqmul1  10632  addmodlteq  10653  frec2uzrdg  10664  frecuzrdgg  10671  seq3val  10715  seqvalcd  10716  seq3fveq2  10730  seqfveq2g  10732  seqfveqg  10733  seq3fveq  10734  seq3feq  10735  seq3shft2  10736  seqshft2g  10737  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seqcaopr3g  10747  seq3caopr2  10748  seqcaopr2g  10749  iseqf1olemkle  10752  iseqf1olemklt  10753  iseqf1olemqk  10762  seq3f1olemqsum  10768  seq3f1olemstep  10769  seq3f1olemp  10770  seq3f1oleml  10771  seqf1oglem2a  10773  seqf1oglem2  10775  seqf1og  10776  seq3id  10780  seq3id2  10781  seq3homo  10782  seqhomog  10785  seqfeq4g  10786  mulexp  10833  expadd  10836  expmul  10839  modqexp  10921  nn0opth2d  10978  bcpasc  11021  hashennn  11035  hashen  11039  omgadd  11058  hashfzo  11079  hashfzp1  11081  hashxp  11083  hashfacen  11093  seq3coll  11099  eqs1  11198  swrdspsleq  11241  pfxeq  11270  pfxsuff1eqwrdeq  11273  ccatopth2  11291  cats1un  11295  swrdccatin1  11299  swrdccat3blem  11313  shftvalg  11390  shftval4g  11391  replim  11413  cjreb  11420  cjexp  11447  absexp  11633  recan  11663  minclpr  11791  mingeb  11796  sumeq2  11913  zsumdc  11938  fsum3  11941  fsumf1o  11944  fsum3cvg2  11948  fsumadd  11960  isummulc2  11980  fsum2d  11989  fsummulc2  12002  fsumconst  12008  modfsummod  12012  fsumparts  12024  fsumrelem  12025  fsumiun  12031  binom  12038  bcxmas  12043  isumshft  12044  isumnn0nn  12047  mertenslem2  12090  clim2prod  12093  prodfrecap  12100  prodeq2  12111  zproddc  12133  fprodseq  12137  fprodf1o  12142  prodsnf  12146  fprodfac  12169  fprodabs  12170  fprodconst  12174  fprod2d  12177  fprodrec  12183  fprodmodd  12195  efne0  12232  efexp  12236  demoivreALT  12328  moddvds  12353  bitsinv1  12516  gcddiv  12583  alginv  12612  algfx  12617  lcmneg  12639  lcmid  12645  lcmgcdeq  12648  divgcdcoprm0  12666  cncongr1  12668  cncongr2  12669  nn0gcdsq  12765  crth  12789  eulerthlema  12795  eulerthlemh  12796  pythagtriplem1  12831  pcqmul  12869  pcexp  12875  pcneg  12891  pcmpt  12909  pcfac  12916  1arith  12933  setscomd  13116  ercpbllemg  13406  mgmidmo  13448  mgmlrid  13455  lidrideqd  13457  lidrididd  13458  grpinvalem  13461  grpinva  13462  issgrp  13479  isnsgrp  13482  sgrpass  13484  sgrp1  13487  issgrpd  13488  sgrppropd  13489  ismndd  13513  mndpropd  13516  imasmnd2  13528  mnd1  13531  mnd1id  13532  ismhm  13537  mhmpropd  13542  mhmlin  13543  mhmeql  13568  isgrp  13582  grppropd  13593  isgrpd2e  13596  dfgrp2  13603  isgrpid2  13616  grpidd2  13617  grpinvfvalg  13618  grpinvpropdg  13651  grpidssd  13652  grpinvssd  13653  grpsubrcan  13657  dfgrp3mlem  13674  grplactcnv  13678  imasgrp2  13690  mhmlem  13694  mulgnn0p1  13713  mulgaddcom  13726  mulginvcom  13727  mulgneg2  13736  mulgnnass  13737  mulgnn0ass  13738  mulgass  13739  mhmmulg  13743  isghm  13823  ghmlin  13828  ghmeql  13847  iscmn  13873  cmnpropd  13875  iscmnd  13878  abladdsub4  13894  imasabl  13916  gsumfzconst  13921  isrng  13940  rngass  13945  rngdi  13946  rngdir  13947  rngpropd  13961  imasrng  13962  issrg  13971  srgmulgass  13995  srgpcomp  13996  srg1expzeq1  14001  isring  14006  iscrng2  14021  ringpropd  14044  ringinvnz1ne0  14055  mulgass2  14064  ring1  14065  imasring  14070  opprnegg  14089  dvdsrd  14101  dvreq1  14149  rhmmul  14171  isrhm2d  14172  rhmopp  14183  rhmunitinv  14185  islring  14199  rrgval  14269  unitrrg  14274  opprdomnbg  14281  islmod  14298  lmodlema  14299  islmodd  14300  lmodvsmmulgdi  14330  lmodprop2d  14355  rmodislmodlem  14357  rmodislmod  14358  rnglidlmsgrp  14504  rnglidlrng  14505  quscrng  14540  cnfldmulg  14583  cnfldexp  14584  gsumfzfsumlemm  14594  zndvds  14656  znf1o  14658  znunit  14666  psr1clfi  14695  txcnp  14988  cnmpt11  15000  cnmpt21  15008  cnmptcom  15015  isxms  15168  xmspropd  15194  bdmopn  15221  dvexp  15428  dvmptfsum  15442  rpcxpmul2  15630  wilthlem1  15697  mpodvdsmulf1o  15707  fsumdvdsmul  15708  perfect  15718  lgsne0  15760  gausslemma2d  15791  lgseisenlem2  15793  lgsquad2lem2  15804  2lgslem1a  15810  2lgslem1b  15811  usgredg2v  16068  wkslem1  16131  wkslem2  16132  iswlk  16134  uspgr2wlkeq  16176  2wlklem  16185  wlkres  16188  nninffeq  16572