Theorem eqeq12d 2192

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  cdeqeq  2959  sbceqg  3075  csbing  3344  uniprg  3826  unisng  3828  intprg  3879  iununir  3972  csbopabg  4083  undifexmid  4195  exmidundif  4208  exmidundifim  4209  limeq  4379  onsucuni2  4565  ordpwsucexmid  4571  csbima12g  4991  dmsnsnsng  5108  cnvsng  5116  csbiotag  5211  fvmptf  5610  eqfnfv2f  5619  fvreseq  5621  fmptco  5684  fnressn  5704  fvsng  5714  cocan1  5790  cocan2  5791  fliftfun  5799  csbriotag  5845  oveqrspc2v  5904  csbov123g  5915  eqfnov  5983  ovmpos  6000  ov2gf  6001  ovmpodxf  6002  caovcomg  6032  caovassg  6035  caovcang  6038  caovcanrd  6040  caovcan  6041  caovdig  6051  caovdirg  6054  caovimo  6070  offveqb  6104  op1stg  6153  op2ndg  6154  f1o2ndf1  6231  tfrlem1  6311  tfrlem3ag  6312  tfrlem3a  6313  tfrlem5  6317  tfrlem9  6322  tfr0dm  6325  tfrlemiubacc  6333  tfrlemiex  6334  tfrlemi1  6335  tfr1onlem3ag  6340  tfr1onlemubacc  6349  tfr1onlemex  6350  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemubacc  6362  tfrcllemex  6363  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  tfri3  6370  rdg0g  6391  frecrdg  6411  nna0r  6481  nnacom  6487  nnaass  6488  nndi  6489  nnmass  6490  nnmsucr  6491  nnmcom  6492  ecopovtrn  6634  ecopovsymg  6636  ecopovtrng  6637  ecovcom  6644  ecovicom  6645  ecovass  6646  ecoviass  6647  ecovdi  6648  ecovidi  6649  dom2lem  6774  ordiso2  7036  inl11  7066  updjud  7083  omp1eomlem  7095  difinfsnlem  7100  nnnninfeq  7128  nninfwlporlemd  7172  nninfwlpor  7174  exmidfodomrlemrALT  7204  exmidaclem  7209  addcanpig  7335  mulcanpig  7336  mulcmpblnq  7369  mulpipqqs  7374  ordpipqqs  7375  mulidnq  7390  enq0sym  7433  nqnq0  7442  mulcmpblnq0  7445  distrnq0  7460  mulcomnq0  7461  addassnq0  7463  nq02m  7466  genipv  7510  cauappcvgprlemladd  7659  addcmpblnr  7740  0idsr  7768  1idsr  7769  axaddcom  7871  ax1rid  7878  ax0id  7879  rereceu  7890  axcaucvg  7901  mulrid  7956  readdcan  8099  cnegexlem1  8134  cnegexlem3  8136  addcan  8139  addcan2  8140  apti  8581  mulcanapd  8620  mulcanap2d  8621  div11ap  8659  divmuleqap  8676  conjmulap  8688  eqneg  8691  cnref1o  9652  fzsuc2  10081  fzprval  10084  fztpval  10085  qtri3or  10245  modqadd1  10363  modqmul1  10379  addmodlteq  10400  frec2uzrdg  10411  frecuzrdgg  10418  seq3val  10460  seqvalcd  10461  seq3fveq2  10471  seq3fveq  10473  seq3feq  10474  seq3shft2  10475  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  iseqf1olemkle  10486  iseqf1olemklt  10487  iseqf1olemqk  10496  seq3f1olemqsum  10502  seq3f1olemstep  10503  seq3f1olemp  10504  seq3f1oleml  10505  seq3id  10510  seq3id2  10511  seq3homo  10512  mulexp  10561  expadd  10564  expmul  10567  modqexp  10649  nn0opth2d  10705  bcpasc  10748  hashennn  10762  hashen  10766  omgadd  10784  hashfzo  10804  hashfzp1  10806  hashxp  10808  hashfacen  10818  seq3coll  10824  shftvalg  10847  shftval4g  10848  replim  10870  cjreb  10877  cjexp  10904  absexp  11090  recan  11120  minclpr  11247  mingeb  11252  sumeq2  11369  zsumdc  11394  fsum3  11397  fsumf1o  11400  fsum3cvg2  11404  fsumadd  11416  isummulc2  11436  fsum2d  11445  fsummulc2  11458  fsumconst  11464  modfsummod  11468  fsumparts  11480  fsumrelem  11481  fsumiun  11487  binom  11494  bcxmas  11499  isumshft  11500  isumnn0nn  11503  mertenslem2  11546  clim2prod  11549  prodfrecap  11556  prodeq2  11567  zproddc  11589  fprodseq  11593  fprodf1o  11598  prodsnf  11602  fprodfac  11625  fprodabs  11626  fprodconst  11630  fprod2d  11633  fprodrec  11639  fprodmodd  11651  efne0  11688  efexp  11692  demoivreALT  11783  moddvds  11808  gcddiv  12022  alginv  12049  algfx  12054  lcmneg  12076  lcmid  12082  lcmgcdeq  12085  divgcdcoprm0  12103  cncongr1  12105  cncongr2  12106  nn0gcdsq  12202  crth  12226  eulerthlema  12232  eulerthlemh  12233  pythagtriplem1  12267  pcqmul  12305  pcexp  12311  pcneg  12326  pcmpt  12343  pcfac  12350  1arith  12367  setscomd  12505  ercpbllemg  12754  mgmidmo  12796  mgmlrid  12803  lidrideqd  12805  lidrididd  12806  grprinvlem  12809  grprinvd  12810  issgrp  12814  isnsgrp  12817  sgrpass  12819  sgrp1  12821  ismndd  12843  mndpropd  12846  mnd1  12852  mnd1id  12853  ismhm  12858  mhmpropd  12862  mhmlin  12863  mhmeql  12881  isgrp  12888  grppropd  12898  isgrpd2e  12901  dfgrp2  12907  isgrpid2  12918  grpidd2  12919  grpinvfvalg  12920  grpinvpropdg  12950  grpidssd  12951  grpinvssd  12952  grpsubrcan  12956  dfgrp3mlem  12973  grplactcnv  12977  mhmlem  12983  mulgnn0p1  12999  mulgaddcom  13012  mulginvcom  13013  mulgneg2  13022  mulgnnass  13023  mulgnn0ass  13024  mulgass  13025  mhmmulg  13029  iscmn  13101  cmnpropd  13103  iscmnd  13106  abladdsub4  13122  issrg  13153  srgmulgass  13177  srgpcomp  13178  srg1expzeq1  13183  isring  13188  iscrng2  13203  ringpropd  13222  ringinvnz1ne0  13231  mulgass2  13240  ring1  13241  opprnegg  13258  dvdsrd  13268  dvreq1  13316  islring  13338  islmod  13386  lmodlema  13387  islmodd  13388  lmodvsmmulgdi  13418  lmodprop2d  13443  rmodislmodlem  13445  rmodislmod  13446  cnfldmulg  13509  cnfldexp  13510  txcnp  13810  cnmpt11  13822  cnmpt21  13830  cnmptcom  13837  isxms  13990  xmspropd  14016  bdmopn  14043  dvexp  14214  lgsne0  14478  lgseisenlem2  14490  nninffeq  14808