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  2981  sbceqg  3097  csbing  3367  uniprg  3851  unisng  3853  intprg  3904  iununir  3997  csbopabg  4108  undifexmid  4223  exmidundif  4236  exmidundifim  4237  limeq  4409  onsucuni2  4597  ordpwsucexmid  4603  csbima12g  5027  dmsnsnsng  5144  cnvsng  5152  csbiotag  5248  fvmptf  5651  eqfnfv2f  5660  fvreseq  5662  fmptco  5725  fnressn  5745  fvsng  5755  cocan1  5831  cocan2  5832  fliftfun  5840  csbriotag  5887  oveqrspc2v  5946  csbov123g  5957  eqfnov  6026  ovmpos  6043  ov2gf  6044  ovmpodxf  6045  caovcomg  6076  caovassg  6079  caovcang  6082  caovcanrd  6084  caovcan  6085  caovdig  6095  caovdirg  6098  caovimo  6114  offveqb  6152  op1stg  6205  op2ndg  6206  f1o2ndf1  6283  tfrlem1  6363  tfrlem3ag  6364  tfrlem3a  6365  tfrlem5  6369  tfrlem9  6374  tfr0dm  6377  tfrlemiubacc  6385  tfrlemiex  6386  tfrlemi1  6387  tfr1onlem3ag  6392  tfr1onlemubacc  6401  tfr1onlemex  6402  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemubacc  6414  tfrcllemex  6415  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  tfri3  6422  rdg0g  6443  frecrdg  6463  nna0r  6533  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  ecopovtrn  6688  ecopovsymg  6690  ecopovtrng  6691  ecovcom  6698  ecovicom  6699  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  dom2lem  6828  ordiso2  7096  inl11  7126  updjud  7143  omp1eomlem  7155  difinfsnlem  7160  nnnninfeq  7189  nninfwlporlemd  7233  nninfwlpor  7235  exmidfodomrlemrALT  7265  exmidaclem  7270  addcanpig  7396  mulcanpig  7397  mulcmpblnq  7430  mulpipqqs  7435  ordpipqqs  7436  mulidnq  7451  enq0sym  7494  nqnq0  7503  mulcmpblnq0  7506  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  nq02m  7527  genipv  7571  cauappcvgprlemladd  7720  addcmpblnr  7801  0idsr  7829  1idsr  7830  axaddcom  7932  ax1rid  7939  ax0id  7940  rereceu  7951  axcaucvg  7962  mulrid  8018  readdcan  8161  cnegexlem1  8196  cnegexlem3  8198  addcan  8201  addcan2  8202  apti  8643  mulcanapd  8682  mulcanap2d  8683  div11ap  8721  divmuleqap  8738  conjmulap  8750  eqneg  8753  cnref1o  9719  fzsuc2  10148  fzprval  10151  fztpval  10152  qtri3or  10313  modqadd1  10435  modqmul1  10451  addmodlteq  10472  frec2uzrdg  10483  frecuzrdgg  10490  seq3val  10534  seqvalcd  10535  seq3fveq2  10549  seqfveq2g  10551  seqfveqg  10552  seq3fveq  10553  seq3feq  10554  seq3shft2  10555  seqshft2g  10556  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqk  10581  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1olemp  10589  seq3f1oleml  10590  seqf1oglem2a  10592  seqf1oglem2  10594  seqf1og  10595  seq3id  10599  seq3id2  10600  seq3homo  10601  seqhomog  10604  seqfeq4g  10605  mulexp  10652  expadd  10655  expmul  10658  modqexp  10740  nn0opth2d  10797  bcpasc  10840  hashennn  10854  hashen  10858  omgadd  10876  hashfzo  10896  hashfzp1  10898  hashxp  10900  hashfacen  10910  seq3coll  10916  shftvalg  10983  shftval4g  10984  replim  11006  cjreb  11013  cjexp  11040  absexp  11226  recan  11256  minclpr  11383  mingeb  11388  sumeq2  11505  zsumdc  11530  fsum3  11533  fsumf1o  11536  fsum3cvg2  11540  fsumadd  11552  isummulc2  11572  fsum2d  11581  fsummulc2  11594  fsumconst  11600  modfsummod  11604  fsumparts  11616  fsumrelem  11617  fsumiun  11623  binom  11630  bcxmas  11635  isumshft  11636  isumnn0nn  11639  mertenslem2  11682  clim2prod  11685  prodfrecap  11692  prodeq2  11703  zproddc  11725  fprodseq  11729  fprodf1o  11734  prodsnf  11738  fprodfac  11761  fprodabs  11762  fprodconst  11766  fprod2d  11769  fprodrec  11775  fprodmodd  11787  efne0  11824  efexp  11828  demoivreALT  11920  moddvds  11945  gcddiv  12159  alginv  12188  algfx  12193  lcmneg  12215  lcmid  12221  lcmgcdeq  12224  divgcdcoprm0  12242  cncongr1  12244  cncongr2  12245  nn0gcdsq  12341  crth  12365  eulerthlema  12371  eulerthlemh  12372  pythagtriplem1  12406  pcqmul  12444  pcexp  12450  pcneg  12466  pcmpt  12484  pcfac  12491  1arith  12508  setscomd  12662  ercpbllemg  12916  mgmidmo  12958  mgmlrid  12965  lidrideqd  12967  lidrididd  12968  grpinvalem  12971  grpinva  12972  issgrp  12989  isnsgrp  12992  sgrpass  12994  sgrp1  12997  issgrpd  12998  sgrppropd  12999  ismndd  13021  mndpropd  13024  mnd1  13030  mnd1id  13031  ismhm  13036  mhmpropd  13041  mhmlin  13042  mhmeql  13067  isgrp  13081  grppropd  13092  isgrpd2e  13095  dfgrp2  13102  isgrpid2  13115  grpidd2  13116  grpinvfvalg  13117  grpinvpropdg  13150  grpidssd  13151  grpinvssd  13152  grpsubrcan  13156  dfgrp3mlem  13173  grplactcnv  13177  imasgrp2  13183  mhmlem  13187  mulgnn0p1  13206  mulgaddcom  13219  mulginvcom  13220  mulgneg2  13229  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  mhmmulg  13236  isghm  13316  ghmlin  13321  ghmeql  13340  iscmn  13366  cmnpropd  13368  iscmnd  13371  abladdsub4  13387  imasabl  13409  gsumfzconst  13414  isrng  13433  rngass  13438  rngdi  13439  rngdir  13440  rngpropd  13454  imasrng  13455  issrg  13464  srgmulgass  13488  srgpcomp  13489  srg1expzeq1  13494  isring  13499  iscrng2  13514  ringpropd  13537  ringinvnz1ne0  13548  mulgass2  13557  ring1  13558  imasring  13563  opprnegg  13582  dvdsrd  13593  dvreq1  13641  rhmmul  13663  isrhm2d  13664  rhmopp  13675  rhmunitinv  13677  islring  13691  rrgval  13761  unitrrg  13766  opprdomnbg  13773  islmod  13790  lmodlema  13791  islmodd  13792  lmodvsmmulgdi  13822  lmodprop2d  13847  rmodislmodlem  13849  rmodislmod  13850  rnglidlmsgrp  13996  rnglidlrng  13997  quscrng  14032  cnfldmulg  14075  cnfldexp  14076  gsumfzfsumlemm  14086  zndvds  14148  znf1o  14150  znunit  14158  txcnp  14450  cnmpt11  14462  cnmpt21  14470  cnmptcom  14477  isxms  14630  xmspropd  14656  bdmopn  14683  dvexp  14890  dvmptfsum  14904  wilthlem1  15153  lgsne0  15195  gausslemma2d  15226  lgseisenlem2  15228  lgsquad2lem2  15239  2lgslem1a  15245  2lgslem1b  15246  nninffeq  15580