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  3903  unisng  3905  intprg  3956  iununir  4049  csbopabg  4162  undifexmid  4277  exmidundif  4290  exmidundifim  4291  limeq  4468  onsucuni2  4656  ordpwsucexmid  4662  csbima12g  5089  dmsnsnsng  5206  cnvsng  5214  csbiotag  5311  fvmptf  5729  eqfnfv2f  5738  fvreseq  5740  fmptco  5803  fnressn  5829  fvsng  5839  cocan1  5917  cocan2  5918  fliftfun  5926  csbriotag  5974  oveqrspc2v  6034  csbov123g  6046  eqfnov  6117  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  caovcomg  6167  caovassg  6170  caovcang  6173  caovcanrd  6175  caovcan  6176  caovdig  6186  caovdirg  6189  caovimo  6205  offveqb  6244  caofid0l  6251  caofid0r  6252  op1stg  6302  op2ndg  6303  f1o2ndf1  6380  tfrlem1  6460  tfrlem3ag  6461  tfrlem3a  6462  tfrlem5  6466  tfrlem9  6471  tfr0dm  6474  tfrlemiubacc  6482  tfrlemiex  6483  tfrlemi1  6484  tfr1onlem3ag  6489  tfr1onlemubacc  6498  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  tfri3  6519  rdg0g  6540  frecrdg  6560  nna0r  6632  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  ecopovtrn  6787  ecopovsymg  6789  ecopovtrng  6790  ecovcom  6797  ecovicom  6798  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  dom2lem  6931  ordiso2  7210  inl11  7240  updjud  7257  omp1eomlem  7269  difinfsnlem  7274  nnnninfeq  7303  nninfwlporlemd  7347  nninfwlpor  7349  nninfinfwlpo  7355  exmidfodomrlemrALT  7389  exmidaclem  7398  addcanpig  7529  mulcanpig  7530  mulcmpblnq  7563  mulpipqqs  7568  ordpipqqs  7569  mulidnq  7584  enq0sym  7627  nqnq0  7636  mulcmpblnq0  7639  distrnq0  7654  mulcomnq0  7655  addassnq0  7657  nq02m  7660  genipv  7704  cauappcvgprlemladd  7853  addcmpblnr  7934  0idsr  7962  1idsr  7963  axaddcom  8065  ax1rid  8072  ax0id  8073  rereceu  8084  axcaucvg  8095  mulrid  8151  readdcan  8294  cnegexlem1  8329  cnegexlem3  8331  addcan  8334  addcan2  8335  apti  8777  mulcanapd  8816  mulcanap2d  8817  div11ap  8855  divmuleqap  8872  conjmulap  8884  eqneg  8887  cnref1o  9854  fzsuc2  10283  fzprval  10286  fztpval  10287  qtri3or  10468  modqadd1  10591  modqmul1  10607  addmodlteq  10628  frec2uzrdg  10639  frecuzrdgg  10646  seq3val  10690  seqvalcd  10691  seq3fveq2  10705  seqfveq2g  10707  seqfveqg  10708  seq3fveq  10709  seq3feq  10710  seq3shft2  10711  seqshft2g  10712  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seqcaopr3g  10722  seq3caopr2  10723  seqcaopr2g  10724  iseqf1olemkle  10727  iseqf1olemklt  10728  iseqf1olemqk  10737  seq3f1olemqsum  10743  seq3f1olemstep  10744  seq3f1olemp  10745  seq3f1oleml  10746  seqf1oglem2a  10748  seqf1oglem2  10750  seqf1og  10751  seq3id  10755  seq3id2  10756  seq3homo  10757  seqhomog  10760  seqfeq4g  10761  mulexp  10808  expadd  10811  expmul  10814  modqexp  10896  nn0opth2d  10953  bcpasc  10996  hashennn  11010  hashen  11014  omgadd  11032  hashfzo  11052  hashfzp1  11054  hashxp  11056  hashfacen  11066  seq3coll  11072  eqs1  11169  swrdspsleq  11207  pfxeq  11236  pfxsuff1eqwrdeq  11239  ccatopth2  11257  cats1un  11261  swrdccatin1  11265  swrdccat3blem  11279  shftvalg  11355  shftval4g  11356  replim  11378  cjreb  11385  cjexp  11412  absexp  11598  recan  11628  minclpr  11756  mingeb  11761  sumeq2  11878  zsumdc  11903  fsum3  11906  fsumf1o  11909  fsum3cvg2  11913  fsumadd  11925  isummulc2  11945  fsum2d  11954  fsummulc2  11967  fsumconst  11973  modfsummod  11977  fsumparts  11989  fsumrelem  11990  fsumiun  11996  binom  12003  bcxmas  12008  isumshft  12009  isumnn0nn  12012  mertenslem2  12055  clim2prod  12058  prodfrecap  12065  prodeq2  12076  zproddc  12098  fprodseq  12102  fprodf1o  12107  prodsnf  12111  fprodfac  12134  fprodabs  12135  fprodconst  12139  fprod2d  12142  fprodrec  12148  fprodmodd  12160  efne0  12197  efexp  12201  demoivreALT  12293  moddvds  12318  bitsinv1  12481  gcddiv  12548  alginv  12577  algfx  12582  lcmneg  12604  lcmid  12610  lcmgcdeq  12613  divgcdcoprm0  12631  cncongr1  12633  cncongr2  12634  nn0gcdsq  12730  crth  12754  eulerthlema  12760  eulerthlemh  12761  pythagtriplem1  12796  pcqmul  12834  pcexp  12840  pcneg  12856  pcmpt  12874  pcfac  12881  1arith  12898  setscomd  13081  ercpbllemg  13371  mgmidmo  13413  mgmlrid  13420  lidrideqd  13422  lidrididd  13423  grpinvalem  13426  grpinva  13427  issgrp  13444  isnsgrp  13447  sgrpass  13449  sgrp1  13452  issgrpd  13453  sgrppropd  13454  ismndd  13478  mndpropd  13481  imasmnd2  13493  mnd1  13496  mnd1id  13497  ismhm  13502  mhmpropd  13507  mhmlin  13508  mhmeql  13533  isgrp  13547  grppropd  13558  isgrpd2e  13561  dfgrp2  13568  isgrpid2  13581  grpidd2  13582  grpinvfvalg  13583  grpinvpropdg  13616  grpidssd  13617  grpinvssd  13618  grpsubrcan  13622  dfgrp3mlem  13639  grplactcnv  13643  imasgrp2  13655  mhmlem  13659  mulgnn0p1  13678  mulgaddcom  13691  mulginvcom  13692  mulgneg2  13701  mulgnnass  13702  mulgnn0ass  13703  mulgass  13704  mhmmulg  13708  isghm  13788  ghmlin  13793  ghmeql  13812  iscmn  13838  cmnpropd  13840  iscmnd  13843  abladdsub4  13859  imasabl  13881  gsumfzconst  13886  isrng  13905  rngass  13910  rngdi  13911  rngdir  13912  rngpropd  13926  imasrng  13927  issrg  13936  srgmulgass  13960  srgpcomp  13961  srg1expzeq1  13966  isring  13971  iscrng2  13986  ringpropd  14009  ringinvnz1ne0  14020  mulgass2  14029  ring1  14030  imasring  14035  opprnegg  14054  dvdsrd  14066  dvreq1  14114  rhmmul  14136  isrhm2d  14137  rhmopp  14148  rhmunitinv  14150  islring  14164  rrgval  14234  unitrrg  14239  opprdomnbg  14246  islmod  14263  lmodlema  14264  islmodd  14265  lmodvsmmulgdi  14295  lmodprop2d  14320  rmodislmodlem  14322  rmodislmod  14323  rnglidlmsgrp  14469  rnglidlrng  14470  quscrng  14505  cnfldmulg  14548  cnfldexp  14549  gsumfzfsumlemm  14559  zndvds  14621  znf1o  14623  znunit  14631  psr1clfi  14660  txcnp  14953  cnmpt11  14965  cnmpt21  14973  cnmptcom  14980  isxms  15133  xmspropd  15159  bdmopn  15186  dvexp  15393  dvmptfsum  15407  rpcxpmul2  15595  wilthlem1  15662  mpodvdsmulf1o  15672  fsumdvdsmul  15673  perfect  15683  lgsne0  15725  gausslemma2d  15756  lgseisenlem2  15758  lgsquad2lem2  15769  2lgslem1a  15775  2lgslem1b  15776  usgredg2v  16030  wkslem1  16041  wkslem2  16042  iswlk  16044  uspgr2wlkeq  16086  2wlklem  16095  wlkres  16098  nninffeq  16416