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  3902  unisng  3904  intprg  3955  iununir  4048  csbopabg  4161  undifexmid  4276  exmidundif  4289  exmidundifim  4290  limeq  4465  onsucuni2  4653  ordpwsucexmid  4659  csbima12g  5085  dmsnsnsng  5202  cnvsng  5210  csbiotag  5307  fvmptf  5720  eqfnfv2f  5729  fvreseq  5731  fmptco  5794  fnressn  5818  fvsng  5828  cocan1  5904  cocan2  5905  fliftfun  5913  csbriotag  5961  oveqrspc2v  6021  csbov123g  6033  eqfnov  6102  ovmpos  6119  ov2gf  6120  ovmpodxf  6121  caovcomg  6152  caovassg  6155  caovcang  6158  caovcanrd  6160  caovcan  6161  caovdig  6171  caovdirg  6174  caovimo  6190  offveqb  6228  caofid0l  6235  caofid0r  6236  op1stg  6286  op2ndg  6287  f1o2ndf1  6364  tfrlem1  6444  tfrlem3ag  6445  tfrlem3a  6446  tfrlem5  6450  tfrlem9  6455  tfr0dm  6458  tfrlemiubacc  6466  tfrlemiex  6467  tfrlemi1  6468  tfr1onlem3ag  6473  tfr1onlemubacc  6482  tfr1onlemex  6483  tfr1onlemaccex  6484  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllemubacc  6495  tfrcllemex  6496  tfrcllemaccex  6497  tfrcllemres  6498  tfrcldm  6499  tfri3  6503  rdg0g  6524  frecrdg  6544  nna0r  6614  nnacom  6620  nnaass  6621  nndi  6622  nnmass  6623  nnmsucr  6624  nnmcom  6625  ecopovtrn  6769  ecopovsymg  6771  ecopovtrng  6772  ecovcom  6779  ecovicom  6780  ecovass  6781  ecoviass  6782  ecovdi  6783  ecovidi  6784  dom2lem  6913  ordiso2  7190  inl11  7220  updjud  7237  omp1eomlem  7249  difinfsnlem  7254  nnnninfeq  7283  nninfwlporlemd  7327  nninfwlpor  7329  nninfinfwlpo  7335  exmidfodomrlemrALT  7369  exmidaclem  7378  addcanpig  7509  mulcanpig  7510  mulcmpblnq  7543  mulpipqqs  7548  ordpipqqs  7549  mulidnq  7564  enq0sym  7607  nqnq0  7616  mulcmpblnq0  7619  distrnq0  7634  mulcomnq0  7635  addassnq0  7637  nq02m  7640  genipv  7684  cauappcvgprlemladd  7833  addcmpblnr  7914  0idsr  7942  1idsr  7943  axaddcom  8045  ax1rid  8052  ax0id  8053  rereceu  8064  axcaucvg  8075  mulrid  8131  readdcan  8274  cnegexlem1  8309  cnegexlem3  8311  addcan  8314  addcan2  8315  apti  8757  mulcanapd  8796  mulcanap2d  8797  div11ap  8835  divmuleqap  8852  conjmulap  8864  eqneg  8867  cnref1o  9834  fzsuc2  10263  fzprval  10266  fztpval  10267  qtri3or  10447  modqadd1  10570  modqmul1  10586  addmodlteq  10607  frec2uzrdg  10618  frecuzrdgg  10625  seq3val  10669  seqvalcd  10670  seq3fveq2  10684  seqfveq2g  10686  seqfveqg  10687  seq3fveq  10688  seq3feq  10689  seq3shft2  10690  seqshft2g  10691  seq3split  10697  seqsplitg  10698  seq3caopr3  10700  seqcaopr3g  10701  seq3caopr2  10702  seqcaopr2g  10703  iseqf1olemkle  10706  iseqf1olemklt  10707  iseqf1olemqk  10716  seq3f1olemqsum  10722  seq3f1olemstep  10723  seq3f1olemp  10724  seq3f1oleml  10725  seqf1oglem2a  10727  seqf1oglem2  10729  seqf1og  10730  seq3id  10734  seq3id2  10735  seq3homo  10736  seqhomog  10739  seqfeq4g  10740  mulexp  10787  expadd  10790  expmul  10793  modqexp  10875  nn0opth2d  10932  bcpasc  10975  hashennn  10989  hashen  10993  omgadd  11011  hashfzo  11031  hashfzp1  11033  hashxp  11035  hashfacen  11045  seq3coll  11051  eqs1  11147  swrdspsleq  11185  pfxeq  11214  pfxsuff1eqwrdeq  11217  ccatopth2  11235  cats1un  11239  swrdccatin1  11243  swrdccat3blem  11257  shftvalg  11333  shftval4g  11334  replim  11356  cjreb  11363  cjexp  11390  absexp  11576  recan  11606  minclpr  11734  mingeb  11739  sumeq2  11856  zsumdc  11881  fsum3  11884  fsumf1o  11887  fsum3cvg2  11891  fsumadd  11903  isummulc2  11923  fsum2d  11932  fsummulc2  11945  fsumconst  11951  modfsummod  11955  fsumparts  11967  fsumrelem  11968  fsumiun  11974  binom  11981  bcxmas  11986  isumshft  11987  isumnn0nn  11990  mertenslem2  12033  clim2prod  12036  prodfrecap  12043  prodeq2  12054  zproddc  12076  fprodseq  12080  fprodf1o  12085  prodsnf  12089  fprodfac  12112  fprodabs  12113  fprodconst  12117  fprod2d  12120  fprodrec  12126  fprodmodd  12138  efne0  12175  efexp  12179  demoivreALT  12271  moddvds  12296  bitsinv1  12459  gcddiv  12526  alginv  12555  algfx  12560  lcmneg  12582  lcmid  12588  lcmgcdeq  12591  divgcdcoprm0  12609  cncongr1  12611  cncongr2  12612  nn0gcdsq  12708  crth  12732  eulerthlema  12738  eulerthlemh  12739  pythagtriplem1  12774  pcqmul  12812  pcexp  12818  pcneg  12834  pcmpt  12852  pcfac  12859  1arith  12876  setscomd  13059  ercpbllemg  13349  mgmidmo  13391  mgmlrid  13398  lidrideqd  13400  lidrididd  13401  grpinvalem  13404  grpinva  13405  issgrp  13422  isnsgrp  13425  sgrpass  13427  sgrp1  13430  issgrpd  13431  sgrppropd  13432  ismndd  13456  mndpropd  13459  imasmnd2  13471  mnd1  13474  mnd1id  13475  ismhm  13480  mhmpropd  13485  mhmlin  13486  mhmeql  13511  isgrp  13525  grppropd  13536  isgrpd2e  13539  dfgrp2  13546  isgrpid2  13559  grpidd2  13560  grpinvfvalg  13561  grpinvpropdg  13594  grpidssd  13595  grpinvssd  13596  grpsubrcan  13600  dfgrp3mlem  13617  grplactcnv  13621  imasgrp2  13633  mhmlem  13637  mulgnn0p1  13656  mulgaddcom  13669  mulginvcom  13670  mulgneg2  13679  mulgnnass  13680  mulgnn0ass  13681  mulgass  13682  mhmmulg  13686  isghm  13766  ghmlin  13771  ghmeql  13790  iscmn  13816  cmnpropd  13818  iscmnd  13821  abladdsub4  13837  imasabl  13859  gsumfzconst  13864  isrng  13883  rngass  13888  rngdi  13889  rngdir  13890  rngpropd  13904  imasrng  13905  issrg  13914  srgmulgass  13938  srgpcomp  13939  srg1expzeq1  13944  isring  13949  iscrng2  13964  ringpropd  13987  ringinvnz1ne0  13998  mulgass2  14007  ring1  14008  imasring  14013  opprnegg  14032  dvdsrd  14043  dvreq1  14091  rhmmul  14113  isrhm2d  14114  rhmopp  14125  rhmunitinv  14127  islring  14141  rrgval  14211  unitrrg  14216  opprdomnbg  14223  islmod  14240  lmodlema  14241  islmodd  14242  lmodvsmmulgdi  14272  lmodprop2d  14297  rmodislmodlem  14299  rmodislmod  14300  rnglidlmsgrp  14446  rnglidlrng  14447  quscrng  14482  cnfldmulg  14525  cnfldexp  14526  gsumfzfsumlemm  14536  zndvds  14598  znf1o  14600  znunit  14608  psr1clfi  14637  txcnp  14930  cnmpt11  14942  cnmpt21  14950  cnmptcom  14957  isxms  15110  xmspropd  15136  bdmopn  15163  dvexp  15370  dvmptfsum  15384  rpcxpmul2  15572  wilthlem1  15639  mpodvdsmulf1o  15649  fsumdvdsmul  15650  perfect  15660  lgsne0  15702  gausslemma2d  15733  lgseisenlem2  15735  lgsquad2lem2  15746  2lgslem1a  15752  2lgslem1b  15753  usgredg2v  16007  nninffeq  16317