Theorem eqeq12d 2180

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  cdeqeq  2946  sbceqg  3061  csbing  3329  uniprg  3804  unisng  3806  intprg  3857  iununir  3949  csbopabg  4060  undifexmid  4172  exmidundif  4185  exmidundifim  4186  limeq  4355  onsucuni2  4541  ordpwsucexmid  4547  csbima12g  4965  dmsnsnsng  5081  cnvsng  5089  csbiotag  5181  fvmptf  5578  eqfnfv2f  5587  fvreseq  5589  fmptco  5651  fnressn  5671  fvsng  5681  cocan1  5755  cocan2  5756  fliftfun  5764  csbriotag  5810  oveqrspc2v  5869  csbov123g  5880  eqfnov  5948  ovmpos  5965  ov2gf  5966  ovmpodxf  5967  caovcomg  5997  caovassg  6000  caovcang  6003  caovcanrd  6005  caovcan  6006  caovdig  6016  caovdirg  6019  caovimo  6035  offveqb  6069  op1stg  6118  op2ndg  6119  f1o2ndf1  6196  tfrlem1  6276  tfrlem3ag  6277  tfrlem3a  6278  tfrlem5  6282  tfrlem9  6287  tfr0dm  6290  tfrlemiubacc  6298  tfrlemiex  6299  tfrlemi1  6300  tfr1onlem3ag  6305  tfr1onlemubacc  6314  tfr1onlemex  6315  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemubacc  6327  tfrcllemex  6328  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  tfri3  6335  rdg0g  6356  frecrdg  6376  nna0r  6446  nnacom  6452  nnaass  6453  nndi  6454  nnmass  6455  nnmsucr  6456  nnmcom  6457  ecopovtrn  6598  ecopovsymg  6600  ecopovtrng  6601  ecovcom  6608  ecovicom  6609  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  dom2lem  6738  ordiso2  7000  inl11  7030  updjud  7047  omp1eomlem  7059  difinfsnlem  7064  nnnninfeq  7092  exmidfodomrlemrALT  7159  exmidaclem  7164  addcanpig  7275  mulcanpig  7276  mulcmpblnq  7309  mulpipqqs  7314  ordpipqqs  7315  mulidnq  7330  enq0sym  7373  nqnq0  7382  mulcmpblnq0  7385  distrnq0  7400  mulcomnq0  7401  addassnq0  7403  nq02m  7406  genipv  7450  cauappcvgprlemladd  7599  addcmpblnr  7680  0idsr  7708  1idsr  7709  axaddcom  7811  ax1rid  7818  ax0id  7819  rereceu  7830  axcaucvg  7841  mulid1  7896  readdcan  8038  cnegexlem1  8073  cnegexlem3  8075  addcan  8078  addcan2  8079  apti  8520  mulcanapd  8558  mulcanap2d  8559  div11ap  8596  divmuleqap  8613  conjmulap  8625  eqneg  8628  cnref1o  9588  fzsuc2  10014  fzprval  10017  fztpval  10018  qtri3or  10178  modqadd1  10296  modqmul1  10312  addmodlteq  10333  frec2uzrdg  10344  frecuzrdgg  10351  seq3val  10393  seqvalcd  10394  seq3fveq2  10404  seq3fveq  10406  seq3feq  10407  seq3shft2  10408  seq3split  10414  seq3caopr3  10416  seq3caopr2  10417  iseqf1olemkle  10419  iseqf1olemklt  10420  iseqf1olemqk  10429  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1olemp  10437  seq3f1oleml  10438  seq3id  10443  seq3id2  10444  seq3homo  10445  mulexp  10494  expadd  10497  expmul  10500  modqexp  10581  nn0opth2d  10636  bcpasc  10679  hashennn  10693  hashen  10697  omgadd  10715  hashfzo  10735  hashfzp1  10737  hashxp  10739  hashfacen  10749  seq3coll  10755  shftvalg  10778  shftval4g  10779  replim  10801  cjreb  10808  cjexp  10835  absexp  11021  recan  11051  minclpr  11178  mingeb  11183  sumeq2  11300  zsumdc  11325  fsum3  11328  fsumf1o  11331  fsum3cvg2  11335  fsumadd  11347  isummulc2  11367  fsum2d  11376  fsummulc2  11389  fsumconst  11395  modfsummod  11399  fsumparts  11411  fsumrelem  11412  fsumiun  11418  binom  11425  bcxmas  11430  isumshft  11431  isumnn0nn  11434  mertenslem2  11477  clim2prod  11480  prodfrecap  11487  prodeq2  11498  zproddc  11520  fprodseq  11524  fprodf1o  11529  prodsnf  11533  fprodfac  11556  fprodabs  11557  fprodconst  11561  fprod2d  11564  fprodrec  11570  fprodmodd  11582  efne0  11619  efexp  11623  demoivreALT  11714  moddvds  11739  gcddiv  11952  alginv  11979  algfx  11984  lcmneg  12006  lcmid  12012  lcmgcdeq  12015  divgcdcoprm0  12033  cncongr1  12035  cncongr2  12036  nn0gcdsq  12132  crth  12156  eulerthlema  12162  eulerthlemh  12163  pythagtriplem1  12197  pcqmul  12235  pcexp  12241  pcneg  12256  pcmpt  12273  pcfac  12280  1arith  12297  mgmidmo  12603  mgmlrid  12610  lidrideqd  12612  lidrididd  12613  grprinvlem  12616  grprinvd  12617  txcnp  12911  cnmpt11  12923  cnmpt21  12931  cnmptcom  12938  isxms  13091  xmspropd  13117  bdmopn  13144  dvexp  13315  lgsne0  13579  nninffeq  13900