Theorem eqeq12d 2179

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157

This theorem is referenced by:  cdeqeq  2941  sbceqg  3056  csbing  3324  uniprg  3798  unisng  3800  intprg  3851  iununir  3943  csbopabg  4054  undifexmid  4166  exmidundif  4179  exmidundifim  4180  limeq  4349  onsucuni2  4535  ordpwsucexmid  4541  csbima12g  4959  dmsnsnsng  5075  cnvsng  5083  csbiotag  5175  fvmptf  5572  eqfnfv2f  5581  fvreseq  5583  fmptco  5645  fnressn  5665  fvsng  5675  cocan1  5749  cocan2  5750  fliftfun  5758  csbriotag  5804  csbov123g  5871  eqfnov  5939  ovmpos  5956  ov2gf  5957  ovmpodxf  5958  caovcomg  5988  caovassg  5991  caovcang  5994  caovcanrd  5996  caovcan  5997  caovdig  6007  caovdirg  6010  caovimo  6026  grprinvlem  6027  grprinvd  6028  offveqb  6063  op1stg  6110  op2ndg  6111  f1o2ndf1  6187  tfrlem1  6267  tfrlem3ag  6268  tfrlem3a  6269  tfrlem5  6273  tfrlem9  6278  tfr0dm  6281  tfrlemiubacc  6289  tfrlemiex  6290  tfrlemi1  6291  tfr1onlem3ag  6296  tfr1onlemubacc  6305  tfr1onlemex  6306  tfr1onlemaccex  6307  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllemubacc  6318  tfrcllemex  6319  tfrcllemaccex  6320  tfrcllemres  6321  tfrcldm  6322  tfri3  6326  rdg0g  6347  frecrdg  6367  nna0r  6437  nnacom  6443  nnaass  6444  nndi  6445  nnmass  6446  nnmsucr  6447  nnmcom  6448  ecopovtrn  6589  ecopovsymg  6591  ecopovtrng  6592  ecovcom  6599  ecovicom  6600  ecovass  6601  ecoviass  6602  ecovdi  6603  ecovidi  6604  dom2lem  6729  ordiso2  6991  inl11  7021  updjud  7038  omp1eomlem  7050  difinfsnlem  7055  nnnninfeq  7083  exmidfodomrlemrALT  7150  exmidaclem  7155  addcanpig  7266  mulcanpig  7267  mulcmpblnq  7300  mulpipqqs  7305  ordpipqqs  7306  mulidnq  7321  enq0sym  7364  nqnq0  7373  mulcmpblnq0  7376  distrnq0  7391  mulcomnq0  7392  addassnq0  7394  nq02m  7397  genipv  7441  cauappcvgprlemladd  7590  addcmpblnr  7671  0idsr  7699  1idsr  7700  axaddcom  7802  ax1rid  7809  ax0id  7810  rereceu  7821  axcaucvg  7832  mulid1  7887  readdcan  8029  cnegexlem1  8064  cnegexlem3  8066  addcan  8069  addcan2  8070  apti  8511  mulcanapd  8549  mulcanap2d  8550  div11ap  8587  divmuleqap  8604  conjmulap  8616  eqneg  8619  cnref1o  9579  fzsuc2  10004  fzprval  10007  fztpval  10008  qtri3or  10168  modqadd1  10286  modqmul1  10302  addmodlteq  10323  frec2uzrdg  10334  frecuzrdgg  10341  seq3val  10383  seqvalcd  10384  seq3fveq2  10394  seq3fveq  10396  seq3feq  10397  seq3shft2  10398  seq3split  10404  seq3caopr3  10406  seq3caopr2  10407  iseqf1olemkle  10409  iseqf1olemklt  10410  iseqf1olemqk  10419  seq3f1olemqsum  10425  seq3f1olemstep  10426  seq3f1olemp  10427  seq3f1oleml  10428  seq3id  10433  seq3id2  10434  seq3homo  10435  mulexp  10484  expadd  10487  expmul  10490  modqexp  10570  nn0opth2d  10625  bcpasc  10668  hashennn  10682  hashen  10686  omgadd  10704  hashfzo  10724  hashfzp1  10726  hashxp  10728  hashfacen  10735  seq3coll  10741  shftvalg  10764  shftval4g  10765  replim  10787  cjreb  10794  cjexp  10821  absexp  11007  recan  11037  minclpr  11164  mingeb  11169  sumeq2  11286  zsumdc  11311  fsum3  11314  fsumf1o  11317  fsum3cvg2  11321  fsumadd  11333  isummulc2  11353  fsum2d  11362  fsummulc2  11375  fsumconst  11381  modfsummod  11385  fsumparts  11397  fsumrelem  11398  fsumiun  11404  binom  11411  bcxmas  11416  isumshft  11417  isumnn0nn  11420  mertenslem2  11463  clim2prod  11466  prodfrecap  11473  prodeq2  11484  zproddc  11506  fprodseq  11510  fprodf1o  11515  prodsnf  11519  fprodfac  11542  fprodabs  11543  fprodconst  11547  fprod2d  11550  fprodrec  11556  fprodmodd  11568  efne0  11605  efexp  11609  demoivreALT  11700  moddvds  11725  gcddiv  11937  alginv  11958  algfx  11963  lcmneg  11985  lcmid  11991  lcmgcdeq  11994  divgcdcoprm0  12012  cncongr1  12014  cncongr2  12015  nn0gcdsq  12109  crth  12133  eulerthlema  12139  eulerthlemh  12140  pythagtriplem1  12174  pcqmul  12212  pcexp  12218  pcneg  12233  pcmpt  12250  pcfac  12257  txcnp  12812  cnmpt11  12824  cnmpt21  12832  cnmptcom  12839  isxms  12992  xmspropd  13018  bdmopn  13045  dvexp  13216  nninffeq  13734