Theorem eqeq12d 2253

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3950  unisng  3952  intprg  4003  iununir  4096  csbopabg  4209  undifexmid  4330  exmidundif  4343  exmidundifim  4344  limeq  4522  onsucuni2  4711  ordpwsucexmid  4717  csbima12g  5148  dmsnsnsng  5265  cnvsng  5273  csbiotag  5370  fvmptf  5798  eqfnfv2f  5810  fvreseq  5812  fmptco  5874  fnressn  5901  fvsng  5911  cocan1  5993  cocan2  5994  fliftfun  6002  csbriotag  6052  oveqrspc2v  6112  csbov123g  6124  eqfnov  6195  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  caovcomg  6245  caovassg  6248  caovcang  6251  caovcanrd  6253  caovcan  6254  caovdig  6264  caovdirg  6267  caovimo  6283  offveqb  6322  caofid0l  6329  caofid0r  6330  op1stg  6384  op2ndg  6385  f1o2ndf1  6464  tfrlem1  6579  tfrlem3ag  6580  tfrlem3a  6581  tfrlem5  6585  tfrlem9  6590  tfr0dm  6593  tfrlemiubacc  6601  tfrlemiex  6602  tfrlemi1  6603  tfr1onlem3ag  6608  tfr1onlemubacc  6617  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemubacc  6630  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfri3  6638  rdg0g  6659  frecrdg  6679  nna0r  6751  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  dom2lem  7058  ordiso2  7375  inl11  7405  updjud  7422  omp1eomlem  7434  difinfsnlem  7439  nnnninfeq  7468  nninfwlporlemd  7512  nninfwlpor  7514  nninfinfwlpo  7520  exmidfodomrlemrALT  7555  exmidaclem  7564  addcanpig  7701  mulcanpig  7702  mulcmpblnq  7735  mulpipqqs  7740  ordpipqqs  7741  mulidnq  7756  enq0sym  7799  nqnq0  7808  mulcmpblnq0  7811  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  nq02m  7832  genipv  7876  cauappcvgprlemladd  8025  addcmpblnr  8106  0idsr  8134  1idsr  8135  axaddcom  8237  ax1rid  8244  ax0id  8245  rereceu  8256  axcaucvg  8267  mulrid  8323  readdcan  8466  cnegexlem1  8501  cnegexlem3  8503  addcan  8506  addcan2  8507  apti  8951  mulcanapd  8990  mulcanap2d  8991  div11ap  9031  divmuleqap  9048  conjmulap  9060  eqneg  9063  cnref1o  10053  fzsuc2  10488  fzprval  10491  fztpval  10492  qtri3or  10677  modqadd1  10800  modqmul1  10816  addmodlteq  10837  frec2uzrdg  10848  frecuzrdgg  10855  seq3val  10899  seqvalcd  10900  seq3fveq2  10914  seqfveq2g  10916  seqfveqg  10917  seq3fveq  10918  seq3feq  10919  seq3shft2  10920  seqshft2g  10921  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seqcaopr3g  10931  seq3caopr2  10932  seqcaopr2g  10933  iseqf1olemkle  10936  iseqf1olemklt  10937  iseqf1olemqk  10946  seq3f1olemqsum  10952  seq3f1olemstep  10953  seq3f1olemp  10954  seq3f1oleml  10955  seqf1oglem2a  10957  seqf1oglem2  10959  seqf1og  10960  seq3id  10964  seq3id2  10965  seq3homo  10966  seqhomog  10969  seqfeq4g  10970  mulexp  11017  expadd  11020  expmul  11023  modqexp  11106  nn0opth2d  11163  bcpasc  11206  bcm1n  11209  hashennn  11221  hashen  11225  omgadd  11244  hashfzo  11265  hashfzp1  11267  hashxp  11269  hashmap  11270  hashfibclem  11284  hashfibc  11285  hashfacen  11286  hashf1lem1  11287  hashf1lem2  11288  hashf1  11289  seq3coll  11296  eqs1  11398  swrdspsleq  11441  pfxeq  11470  pfxsuff1eqwrdeq  11473  ccatopth2  11491  cats1un  11495  swrdccatin1  11499  swrdccat3blem  11513  shftvalg  11603  shftval4g  11604  replim  11626  cjreb  11633  cjexp  11660  absexp  11847  recan  11877  minclpr  12005  mingeb  12010  sumeq2  12127  zsumdc  12153  fsum3  12156  fsumf1o  12159  fsum3cvg2  12163  fsumadd  12175  isummulc2  12195  fsum2d  12204  fsummulc2  12217  fsumconst  12223  modfsummod  12227  fsumparts  12239  fsumrelem  12240  fsumiun  12246  binom  12253  bcxmas  12258  isumshft  12259  isumnn0nn  12262  mertenslem2  12305  clim2prod  12308  prodfrecap  12315  prodeq2  12326  zproddc  12348  fprodseq  12352  fprodf1o  12357  prodsnf  12361  fprodfac  12384  fprodabs  12385  fprodconst  12389  fprod2d  12392  fprodrec  12398  fprodmodd  12410  efne0  12447  efexp  12451  demoivreALT  12543  moddvds  12568  bitsinv1  12731  gcddiv  12798  alginv  12827  algfx  12832  lcmneg  12854  lcmid  12860  lcmgcdeq  12863  divgcdcoprm0  12881  cncongr1  12883  cncongr2  12884  nn0gcdsq  12980  crth  13004  eulerthlema  13010  eulerthlemh  13011  pythagtriplem1  13046  pcqmul  13084  pcexp  13090  pcneg  13106  pcmpt  13124  pcfac  13131  1arith  13148  setscomd  13395  ercpbllemg  13653  mgmidmo  13694  mgmlrid  13701  lidrideqd  13703  lidrididd  13704  grpinvalem  13707  grpinva  13708  issgrp  13720  isnsgrp  13723  sgrpass  13725  sgrp1  13728  issgrpd  13729  sgrppropd  13730  ismndd  13752  mndpropd  13755  imasmnd2  13761  mnd1  13764  mnd1id  13765  ismhm  13770  mhmpropd  13775  mhmlin  13776  mhmeql  13801  isgrp  13813  grppropd  13824  isgrpd2e  13827  dfgrp2  13834  isgrpid2  13847  grpidd2  13848  grpinvfvalg  13849  grpinvpropdg  13882  grpidssd  13883  grpinvssd  13884  grpsubrcan  13888  dfgrp3mlem  13905  grplactcnv  13909  imasgrp2  13915  mhmlem  13919  mulgnn0p1  13938  mulgaddcom  13951  mulginvcom  13952  mulgneg2  13961  mulgnnass  13962  mulgnn0ass  13963  mulgass  13964  mhmmulg  13968  isghm  14048  ghmlin  14053  ghmeql  14072  iscmn  14098  cmnpropd  14100  iscmnd  14103  cmnsubm  14114  abladdsub4  14120  imasabl  14142  gzsumconst  14145  gsummptfidmadd  14163  gsumconstcmn  14168  isrng  14235  rngass  14240  rngdi  14241  rngdir  14242  rngpropd  14256  imasrng  14257  issrg  14271  srgmulgass  14295  srgpcomp  14296  srg1expzeq1  14301  isring  14306  iscrng2  14321  ringpropd  14345  ringinvnz1ne0  14356  mulgass2  14365  ring1  14366  imasring  14371  opprnegg  14391  dvdsrd  14403  dvreq1  14451  rhmmul  14473  isrhm2d  14474  rhmopp  14485  rhmunitinv  14487  islring  14501  opprlring  14506  rrgval  14572  unitrrg  14578  opprdomnbg  14585  islmod  14629  lmodlema  14630  islmodd  14631  lmodvsmmulgdi  14662  lmodprop2d  14687  rmodislmodlem  14689  rmodislmod  14690  rnglidlmsgrp  14836  rnglidlrng  14837  quscrng  14872  cnfldmulg  14915  cnfldexp  14916  gsumfsum  14925  zndvds  14986  znf1o  14988  znunit  14996  isassa  15004  assalem  15005  isassad  15013  assapropd  15016  assamulgscm  15045  psr1clfi  15081  txcnp  15374  cnmpt11  15386  cnmpt21  15394  cnmptcom  15401  isxms  15554  xmspropd  15580  bdmopn  15607  dvexp  15814  dvmptfsum  15828  rpcxpmul2  16021  wilthlem1  16100  mpodvdsmulf1o  16110  fsumdvdsmul  16111  perfect  16121  lgsne0  16169  gausslemma2d  16200  lgseisenlem2  16202  lgsquad2lem2  16213  2lgslem1a  16219  2lgslem1b  16220  usgredg2v  16477  issubgr  16510  wkslem1  16573  wkslem2  16574  iswlk  16576  uspgr2wlkeq  16618  2wlklem  16629  wlkres  16632  eupth2lem3fi  16729  eupth2fi  16732  depindlem1  16759  depindlem2  16760  depindlem3  16761  depind  16762  nninffeq  17075