Theorem eqeq12d 2208

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  cdeqeq  2980  sbceqg  3096  csbing  3366  uniprg  3850  unisng  3852  intprg  3903  iununir  3996  csbopabg  4107  undifexmid  4222  exmidundif  4235  exmidundifim  4236  limeq  4408  onsucuni2  4596  ordpwsucexmid  4602  csbima12g  5026  dmsnsnsng  5143  cnvsng  5151  csbiotag  5247  fvmptf  5650  eqfnfv2f  5659  fvreseq  5661  fmptco  5724  fnressn  5744  fvsng  5754  cocan1  5830  cocan2  5831  fliftfun  5839  csbriotag  5886  oveqrspc2v  5945  csbov123g  5956  eqfnov  6025  ovmpos  6042  ov2gf  6043  ovmpodxf  6044  caovcomg  6074  caovassg  6077  caovcang  6080  caovcanrd  6082  caovcan  6083  caovdig  6093  caovdirg  6096  caovimo  6112  offveqb  6150  op1stg  6203  op2ndg  6204  f1o2ndf1  6281  tfrlem1  6361  tfrlem3ag  6362  tfrlem3a  6363  tfrlem5  6367  tfrlem9  6372  tfr0dm  6375  tfrlemiubacc  6383  tfrlemiex  6384  tfrlemi1  6385  tfr1onlem3ag  6390  tfr1onlemubacc  6399  tfr1onlemex  6400  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemubacc  6412  tfrcllemex  6413  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  tfri3  6420  rdg0g  6441  frecrdg  6461  nna0r  6531  nnacom  6537  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  ecopovtrn  6686  ecopovsymg  6688  ecopovtrng  6689  ecovcom  6696  ecovicom  6697  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  dom2lem  6826  ordiso2  7094  inl11  7124  updjud  7141  omp1eomlem  7153  difinfsnlem  7158  nnnninfeq  7187  nninfwlporlemd  7231  nninfwlpor  7233  exmidfodomrlemrALT  7263  exmidaclem  7268  addcanpig  7394  mulcanpig  7395  mulcmpblnq  7428  mulpipqqs  7433  ordpipqqs  7434  mulidnq  7449  enq0sym  7492  nqnq0  7501  mulcmpblnq0  7504  distrnq0  7519  mulcomnq0  7520  addassnq0  7522  nq02m  7525  genipv  7569  cauappcvgprlemladd  7718  addcmpblnr  7799  0idsr  7827  1idsr  7828  axaddcom  7930  ax1rid  7937  ax0id  7938  rereceu  7949  axcaucvg  7960  mulrid  8016  readdcan  8159  cnegexlem1  8194  cnegexlem3  8196  addcan  8199  addcan2  8200  apti  8641  mulcanapd  8680  mulcanap2d  8681  div11ap  8719  divmuleqap  8736  conjmulap  8748  eqneg  8751  cnref1o  9716  fzsuc2  10145  fzprval  10148  fztpval  10149  qtri3or  10310  modqadd1  10432  modqmul1  10448  addmodlteq  10469  frec2uzrdg  10480  frecuzrdgg  10487  seq3val  10531  seqvalcd  10532  seq3fveq2  10546  seqfveq2g  10548  seqfveqg  10549  seq3fveq  10550  seq3feq  10551  seq3shft2  10552  seqshft2g  10553  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqk  10578  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1olemp  10586  seq3f1oleml  10587  seqf1oglem2a  10589  seqf1oglem2  10591  seqf1og  10592  seq3id  10596  seq3id2  10597  seq3homo  10598  seqhomog  10601  seqfeq4g  10602  mulexp  10649  expadd  10652  expmul  10655  modqexp  10737  nn0opth2d  10794  bcpasc  10837  hashennn  10851  hashen  10855  omgadd  10873  hashfzo  10893  hashfzp1  10895  hashxp  10897  hashfacen  10907  seq3coll  10913  shftvalg  10980  shftval4g  10981  replim  11003  cjreb  11010  cjexp  11037  absexp  11223  recan  11253  minclpr  11380  mingeb  11385  sumeq2  11502  zsumdc  11527  fsum3  11530  fsumf1o  11533  fsum3cvg2  11537  fsumadd  11549  isummulc2  11569  fsum2d  11578  fsummulc2  11591  fsumconst  11597  modfsummod  11601  fsumparts  11613  fsumrelem  11614  fsumiun  11620  binom  11627  bcxmas  11632  isumshft  11633  isumnn0nn  11636  mertenslem2  11679  clim2prod  11682  prodfrecap  11689  prodeq2  11700  zproddc  11722  fprodseq  11726  fprodf1o  11731  prodsnf  11735  fprodfac  11758  fprodabs  11759  fprodconst  11763  fprod2d  11766  fprodrec  11772  fprodmodd  11784  efne0  11821  efexp  11825  demoivreALT  11917  moddvds  11942  gcddiv  12156  alginv  12185  algfx  12190  lcmneg  12212  lcmid  12218  lcmgcdeq  12221  divgcdcoprm0  12239  cncongr1  12241  cncongr2  12242  nn0gcdsq  12338  crth  12362  eulerthlema  12368  eulerthlemh  12369  pythagtriplem1  12403  pcqmul  12441  pcexp  12447  pcneg  12463  pcmpt  12481  pcfac  12488  1arith  12505  setscomd  12659  ercpbllemg  12913  mgmidmo  12955  mgmlrid  12962  lidrideqd  12964  lidrididd  12965  grpinvalem  12968  grpinva  12969  issgrp  12986  isnsgrp  12989  sgrpass  12991  sgrp1  12994  issgrpd  12995  sgrppropd  12996  ismndd  13018  mndpropd  13021  mnd1  13027  mnd1id  13028  ismhm  13033  mhmpropd  13038  mhmlin  13039  mhmeql  13064  isgrp  13078  grppropd  13089  isgrpd2e  13092  dfgrp2  13099  isgrpid2  13112  grpidd2  13113  grpinvfvalg  13114  grpinvpropdg  13147  grpidssd  13148  grpinvssd  13149  grpsubrcan  13153  dfgrp3mlem  13170  grplactcnv  13174  imasgrp2  13180  mhmlem  13184  mulgnn0p1  13203  mulgaddcom  13216  mulginvcom  13217  mulgneg2  13226  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  mhmmulg  13233  isghm  13313  ghmlin  13318  ghmeql  13337  iscmn  13363  cmnpropd  13365  iscmnd  13368  abladdsub4  13384  imasabl  13406  gsumfzconst  13411  isrng  13430  rngass  13435  rngdi  13436  rngdir  13437  rngpropd  13451  imasrng  13452  issrg  13461  srgmulgass  13485  srgpcomp  13486  srg1expzeq1  13491  isring  13496  iscrng2  13511  ringpropd  13534  ringinvnz1ne0  13545  mulgass2  13554  ring1  13555  imasring  13560  opprnegg  13579  dvdsrd  13590  dvreq1  13638  rhmmul  13660  isrhm2d  13661  rhmopp  13672  rhmunitinv  13674  islring  13688  rrgval  13758  unitrrg  13763  opprdomnbg  13770  islmod  13787  lmodlema  13788  islmodd  13789  lmodvsmmulgdi  13819  lmodprop2d  13844  rmodislmodlem  13846  rmodislmod  13847  rnglidlmsgrp  13993  rnglidlrng  13994  quscrng  14029  cnfldmulg  14064  cnfldexp  14065  gsumfzfsumlemm  14075  zndvds  14137  znf1o  14139  znunit  14147  txcnp  14439  cnmpt11  14451  cnmpt21  14459  cnmptcom  14466  isxms  14619  xmspropd  14645  bdmopn  14672  dvexp  14860  wilthlem1  15112  lgsne0  15154  gausslemma2d  15185  lgseisenlem2  15187  nninffeq  15510