Theorem eqeq12d 2185

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

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

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  cdeqeq  2950  sbceqg  3065  csbing  3334  uniprg  3811  unisng  3813  intprg  3864  iununir  3956  csbopabg  4067  undifexmid  4179  exmidundif  4192  exmidundifim  4193  limeq  4362  onsucuni2  4548  ordpwsucexmid  4554  csbima12g  4972  dmsnsnsng  5088  cnvsng  5096  csbiotag  5191  fvmptf  5588  eqfnfv2f  5597  fvreseq  5599  fmptco  5662  fnressn  5682  fvsng  5692  cocan1  5766  cocan2  5767  fliftfun  5775  csbriotag  5821  oveqrspc2v  5880  csbov123g  5891  eqfnov  5959  ovmpos  5976  ov2gf  5977  ovmpodxf  5978  caovcomg  6008  caovassg  6011  caovcang  6014  caovcanrd  6016  caovcan  6017  caovdig  6027  caovdirg  6030  caovimo  6046  offveqb  6080  op1stg  6129  op2ndg  6130  f1o2ndf1  6207  tfrlem1  6287  tfrlem3ag  6288  tfrlem3a  6289  tfrlem5  6293  tfrlem9  6298  tfr0dm  6301  tfrlemiubacc  6309  tfrlemiex  6310  tfrlemi1  6311  tfr1onlem3ag  6316  tfr1onlemubacc  6325  tfr1onlemex  6326  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemubacc  6338  tfrcllemex  6339  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  tfri3  6346  rdg0g  6367  frecrdg  6387  nna0r  6457  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  ecopovtrn  6610  ecopovsymg  6612  ecopovtrng  6613  ecovcom  6620  ecovicom  6621  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  dom2lem  6750  ordiso2  7012  inl11  7042  updjud  7059  omp1eomlem  7071  difinfsnlem  7076  nnnninfeq  7104  nninfwlporlemd  7148  nninfwlpor  7150  exmidfodomrlemrALT  7180  exmidaclem  7185  addcanpig  7296  mulcanpig  7297  mulcmpblnq  7330  mulpipqqs  7335  ordpipqqs  7336  mulidnq  7351  enq0sym  7394  nqnq0  7403  mulcmpblnq0  7406  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  nq02m  7427  genipv  7471  cauappcvgprlemladd  7620  addcmpblnr  7701  0idsr  7729  1idsr  7730  axaddcom  7832  ax1rid  7839  ax0id  7840  rereceu  7851  axcaucvg  7862  mulid1  7917  readdcan  8059  cnegexlem1  8094  cnegexlem3  8096  addcan  8099  addcan2  8100  apti  8541  mulcanapd  8579  mulcanap2d  8580  div11ap  8617  divmuleqap  8634  conjmulap  8646  eqneg  8649  cnref1o  9609  fzsuc2  10035  fzprval  10038  fztpval  10039  qtri3or  10199  modqadd1  10317  modqmul1  10333  addmodlteq  10354  frec2uzrdg  10365  frecuzrdgg  10372  seq3val  10414  seqvalcd  10415  seq3fveq2  10425  seq3fveq  10427  seq3feq  10428  seq3shft2  10429  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqk  10450  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1olemp  10458  seq3f1oleml  10459  seq3id  10464  seq3id2  10465  seq3homo  10466  mulexp  10515  expadd  10518  expmul  10521  modqexp  10602  nn0opth2d  10657  bcpasc  10700  hashennn  10714  hashen  10718  omgadd  10737  hashfzo  10757  hashfzp1  10759  hashxp  10761  hashfacen  10771  seq3coll  10777  shftvalg  10800  shftval4g  10801  replim  10823  cjreb  10830  cjexp  10857  absexp  11043  recan  11073  minclpr  11200  mingeb  11205  sumeq2  11322  zsumdc  11347  fsum3  11350  fsumf1o  11353  fsum3cvg2  11357  fsumadd  11369  isummulc2  11389  fsum2d  11398  fsummulc2  11411  fsumconst  11417  modfsummod  11421  fsumparts  11433  fsumrelem  11434  fsumiun  11440  binom  11447  bcxmas  11452  isumshft  11453  isumnn0nn  11456  mertenslem2  11499  clim2prod  11502  prodfrecap  11509  prodeq2  11520  zproddc  11542  fprodseq  11546  fprodf1o  11551  prodsnf  11555  fprodfac  11578  fprodabs  11579  fprodconst  11583  fprod2d  11586  fprodrec  11592  fprodmodd  11604  efne0  11641  efexp  11645  demoivreALT  11736  moddvds  11761  gcddiv  11974  alginv  12001  algfx  12006  lcmneg  12028  lcmid  12034  lcmgcdeq  12037  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  nn0gcdsq  12154  crth  12178  eulerthlema  12184  eulerthlemh  12185  pythagtriplem1  12219  pcqmul  12257  pcexp  12263  pcneg  12278  pcmpt  12295  pcfac  12302  1arith  12319  mgmidmo  12626  mgmlrid  12633  lidrideqd  12635  lidrididd  12636  grprinvlem  12639  grprinvd  12640  issgrp  12644  isnsgrp  12647  sgrpass  12649  sgrp1  12651  ismndd  12673  mndpropd  12676  mnd1  12679  mnd1id  12680  ismhm  12685  mhmpropd  12689  mhmlin  12690  mhmeql  12707  isgrp  12714  grppropd  12724  isgrpd2e  12726  dfgrp2  12732  isgrpid2  12743  grpidd2  12744  grpinvfvalg  12745  txcnp  13065  cnmpt11  13077  cnmpt21  13085  cnmptcom  13092  isxms  13245  xmspropd  13271  bdmopn  13298  dvexp  13469  lgsne0  13733  nninffeq  14053