Theorem eqeq12d 2221

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  cdeqeq  2995  sbceqg  3111  csbing  3382  uniprg  3868  unisng  3870  intprg  3921  iununir  4014  csbopabg  4127  undifexmid  4242  exmidundif  4255  exmidundifim  4256  limeq  4429  onsucuni2  4617  ordpwsucexmid  4623  csbima12g  5049  dmsnsnsng  5166  cnvsng  5174  csbiotag  5270  fvmptf  5682  eqfnfv2f  5691  fvreseq  5693  fmptco  5756  fnressn  5780  fvsng  5790  cocan1  5866  cocan2  5867  fliftfun  5875  csbriotag  5922  oveqrspc2v  5981  csbov123g  5993  eqfnov  6062  ovmpos  6079  ov2gf  6080  ovmpodxf  6081  caovcomg  6112  caovassg  6115  caovcang  6118  caovcanrd  6120  caovcan  6121  caovdig  6131  caovdirg  6134  caovimo  6150  offveqb  6188  caofid0l  6195  caofid0r  6196  op1stg  6246  op2ndg  6247  f1o2ndf1  6324  tfrlem1  6404  tfrlem3ag  6405  tfrlem3a  6406  tfrlem5  6410  tfrlem9  6415  tfr0dm  6418  tfrlemiubacc  6426  tfrlemiex  6427  tfrlemi1  6428  tfr1onlem3ag  6433  tfr1onlemubacc  6442  tfr1onlemex  6443  tfr1onlemaccex  6444  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllemubacc  6455  tfrcllemex  6456  tfrcllemaccex  6457  tfrcllemres  6458  tfrcldm  6459  tfri3  6463  rdg0g  6484  frecrdg  6504  nna0r  6574  nnacom  6580  nnaass  6581  nndi  6582  nnmass  6583  nnmsucr  6584  nnmcom  6585  ecopovtrn  6729  ecopovsymg  6731  ecopovtrng  6732  ecovcom  6739  ecovicom  6740  ecovass  6741  ecoviass  6742  ecovdi  6743  ecovidi  6744  dom2lem  6873  ordiso2  7149  inl11  7179  updjud  7196  omp1eomlem  7208  difinfsnlem  7213  nnnninfeq  7242  nninfwlporlemd  7286  nninfwlpor  7288  nninfinfwlpo  7294  exmidfodomrlemrALT  7324  exmidaclem  7333  addcanpig  7460  mulcanpig  7461  mulcmpblnq  7494  mulpipqqs  7499  ordpipqqs  7500  mulidnq  7515  enq0sym  7558  nqnq0  7567  mulcmpblnq0  7570  distrnq0  7585  mulcomnq0  7586  addassnq0  7588  nq02m  7591  genipv  7635  cauappcvgprlemladd  7784  addcmpblnr  7865  0idsr  7893  1idsr  7894  axaddcom  7996  ax1rid  8003  ax0id  8004  rereceu  8015  axcaucvg  8026  mulrid  8082  readdcan  8225  cnegexlem1  8260  cnegexlem3  8262  addcan  8265  addcan2  8266  apti  8708  mulcanapd  8747  mulcanap2d  8748  div11ap  8786  divmuleqap  8803  conjmulap  8815  eqneg  8818  cnref1o  9785  fzsuc2  10214  fzprval  10217  fztpval  10218  qtri3or  10396  modqadd1  10519  modqmul1  10535  addmodlteq  10556  frec2uzrdg  10567  frecuzrdgg  10574  seq3val  10618  seqvalcd  10619  seq3fveq2  10633  seqfveq2g  10635  seqfveqg  10636  seq3fveq  10637  seq3feq  10638  seq3shft2  10639  seqshft2g  10640  seq3split  10646  seqsplitg  10647  seq3caopr3  10649  seqcaopr3g  10650  seq3caopr2  10651  seqcaopr2g  10652  iseqf1olemkle  10655  iseqf1olemklt  10656  iseqf1olemqk  10665  seq3f1olemqsum  10671  seq3f1olemstep  10672  seq3f1olemp  10673  seq3f1oleml  10674  seqf1oglem2a  10676  seqf1oglem2  10678  seqf1og  10679  seq3id  10683  seq3id2  10684  seq3homo  10685  seqhomog  10688  seqfeq4g  10689  mulexp  10736  expadd  10739  expmul  10742  modqexp  10824  nn0opth2d  10881  bcpasc  10924  hashennn  10938  hashen  10942  omgadd  10960  hashfzo  10980  hashfzp1  10982  hashxp  10984  hashfacen  10994  seq3coll  11000  eqs1  11096  swrdspsleq  11134  pfxeq  11161  pfxsuff1eqwrdeq  11164  shftvalg  11197  shftval4g  11198  replim  11220  cjreb  11227  cjexp  11254  absexp  11440  recan  11470  minclpr  11598  mingeb  11603  sumeq2  11720  zsumdc  11745  fsum3  11748  fsumf1o  11751  fsum3cvg2  11755  fsumadd  11767  isummulc2  11787  fsum2d  11796  fsummulc2  11809  fsumconst  11815  modfsummod  11819  fsumparts  11831  fsumrelem  11832  fsumiun  11838  binom  11845  bcxmas  11850  isumshft  11851  isumnn0nn  11854  mertenslem2  11897  clim2prod  11900  prodfrecap  11907  prodeq2  11918  zproddc  11940  fprodseq  11944  fprodf1o  11949  prodsnf  11953  fprodfac  11976  fprodabs  11977  fprodconst  11981  fprod2d  11984  fprodrec  11990  fprodmodd  12002  efne0  12039  efexp  12043  demoivreALT  12135  moddvds  12160  bitsinv1  12323  gcddiv  12390  alginv  12419  algfx  12424  lcmneg  12446  lcmid  12452  lcmgcdeq  12455  divgcdcoprm0  12473  cncongr1  12475  cncongr2  12476  nn0gcdsq  12572  crth  12596  eulerthlema  12602  eulerthlemh  12603  pythagtriplem1  12638  pcqmul  12676  pcexp  12682  pcneg  12698  pcmpt  12716  pcfac  12723  1arith  12740  setscomd  12923  ercpbllemg  13212  mgmidmo  13254  mgmlrid  13261  lidrideqd  13263  lidrididd  13264  grpinvalem  13267  grpinva  13268  issgrp  13285  isnsgrp  13288  sgrpass  13290  sgrp1  13293  issgrpd  13294  sgrppropd  13295  ismndd  13319  mndpropd  13322  imasmnd2  13334  mnd1  13337  mnd1id  13338  ismhm  13343  mhmpropd  13348  mhmlin  13349  mhmeql  13374  isgrp  13388  grppropd  13399  isgrpd2e  13402  dfgrp2  13409  isgrpid2  13422  grpidd2  13423  grpinvfvalg  13424  grpinvpropdg  13457  grpidssd  13458  grpinvssd  13459  grpsubrcan  13463  dfgrp3mlem  13480  grplactcnv  13484  imasgrp2  13496  mhmlem  13500  mulgnn0p1  13519  mulgaddcom  13532  mulginvcom  13533  mulgneg2  13542  mulgnnass  13543  mulgnn0ass  13544  mulgass  13545  mhmmulg  13549  isghm  13629  ghmlin  13634  ghmeql  13653  iscmn  13679  cmnpropd  13681  iscmnd  13684  abladdsub4  13700  imasabl  13722  gsumfzconst  13727  isrng  13746  rngass  13751  rngdi  13752  rngdir  13753  rngpropd  13767  imasrng  13768  issrg  13777  srgmulgass  13801  srgpcomp  13802  srg1expzeq1  13807  isring  13812  iscrng2  13827  ringpropd  13850  ringinvnz1ne0  13861  mulgass2  13870  ring1  13871  imasring  13876  opprnegg  13895  dvdsrd  13906  dvreq1  13954  rhmmul  13976  isrhm2d  13977  rhmopp  13988  rhmunitinv  13990  islring  14004  rrgval  14074  unitrrg  14079  opprdomnbg  14086  islmod  14103  lmodlema  14104  islmodd  14105  lmodvsmmulgdi  14135  lmodprop2d  14160  rmodislmodlem  14162  rmodislmod  14163  rnglidlmsgrp  14309  rnglidlrng  14310  quscrng  14345  cnfldmulg  14388  cnfldexp  14389  gsumfzfsumlemm  14399  zndvds  14461  znf1o  14463  znunit  14471  psr1clfi  14500  txcnp  14793  cnmpt11  14805  cnmpt21  14813  cnmptcom  14820  isxms  14973  xmspropd  14999  bdmopn  15026  dvexp  15233  dvmptfsum  15247  rpcxpmul2  15435  wilthlem1  15502  mpodvdsmulf1o  15512  fsumdvdsmul  15513  perfect  15523  lgsne0  15565  gausslemma2d  15596  lgseisenlem2  15598  lgsquad2lem2  15609  2lgslem1a  15615  2lgslem1b  15616  nninffeq  16072