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  7376  inl11  7406  updjud  7423  omp1eomlem  7435  difinfsnlem  7440  nnnninfeq  7469  nninfwlporlemd  7513  nninfwlpor  7515  nninfinfwlpo  7521  exmidfodomrlemrALT  7556  exmidaclem  7565  addcanpig  7702  mulcanpig  7703  mulcmpblnq  7736  mulpipqqs  7741  ordpipqqs  7742  mulidnq  7757  enq0sym  7800  nqnq0  7809  mulcmpblnq0  7812  distrnq0  7827  mulcomnq0  7828  addassnq0  7830  nq02m  7833  genipv  7877  cauappcvgprlemladd  8026  addcmpblnr  8107  0idsr  8135  1idsr  8136  axaddcom  8238  ax1rid  8245  ax0id  8246  rereceu  8257  axcaucvg  8268  mulrid  8324  readdcan  8468  cnegexlem1  8503  cnegexlem3  8505  addcan  8508  addcan2  8509  apti  8953  mulcanapd  8992  mulcanap2d  8993  div11ap  9033  divmuleqap  9050  conjmulap  9062  eqneg  9065  cnref1o  10062  fzsuc2  10497  fzprval  10500  fztpval  10501  qtri3or  10686  modqadd1  10812  modqmul1  10828  addmodlteq  10849  frec2uzrdg  10860  frecuzrdgg  10867  seq3val  10911  seqvalcd  10912  seq3fveq2  10926  seqfveq2g  10928  seqfveqg  10929  seq3fveq  10930  seq3feq  10931  seq3shft2  10932  seqshft2g  10933  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  seq3caopr2  10944  seqcaopr2g  10945  iseqf1olemkle  10948  iseqf1olemklt  10949  iseqf1olemqk  10958  seq3f1olemqsum  10964  seq3f1olemstep  10965  seq3f1olemp  10966  seq3f1oleml  10967  seqf1oglem2a  10969  seqf1oglem2  10971  seqf1og  10972  seq3id  10976  seq3id2  10977  seq3homo  10978  seqhomog  10981  seqfeq4g  10982  mulexp  11029  expadd  11032  expmul  11035  modqexp  11118  nn0opth2d  11176  bcpasc  11219  bcm1n  11222  hashennn  11234  hashen  11238  omgadd  11257  hashfzo  11278  hashfzp1  11280  hashxp  11282  hashmap  11283  hashfibclem  11297  hashfibc  11298  hashfacen  11299  hashf1lem1  11300  hashf1lem2  11301  hashf1  11302  seq3coll  11309  eqs1  11411  swrdspsleq  11454  pfxeq  11483  pfxsuff1eqwrdeq  11486  ccatopth2  11504  cats1un  11508  swrdccatin1  11512  swrdccat3blem  11526  shftvalg  11616  shftval4g  11617  replim  11639  cjreb  11646  cjexp  11673  absexp  11861  recan  11891  minclpr  12020  mingeb  12026  sumeq2  12143  zsumdc  12169  fsum3  12172  fsumf1o  12175  fsum3cvg2  12179  fsumadd  12191  isummulc2  12211  fsum2d  12220  fsummulc2  12233  fsumconst  12239  modfsummod  12243  fsumparts  12255  fsumrelem  12256  fsumiun  12262  binom  12269  bcxmas  12274  isumshft  12275  isumnn0nn  12278  mertenslem2  12321  clim2prod  12324  prodfrecap  12331  prodeq2  12342  zproddc  12364  fprodseq  12368  fprodf1o  12373  prodsnf  12377  fprodfac  12400  fprodabs  12401  fprodconst  12405  fprod2d  12408  fprodrec  12414  fprodmodd  12426  efne0  12463  efexp  12467  demoivreALT  12559  moddvds  12584  bitsinv1  12747  gcddiv  12814  alginv  12843  algfx  12848  lcmneg  12870  lcmid  12876  lcmgcdeq  12879  divgcdcoprm0  12897  cncongr1  12899  cncongr2  12900  nn0gcdsq  12998  crth  13024  eulerthlema  13030  eulerthlemh  13031  pythagtriplem1  13066  pcqmul  13104  pcexp  13110  pcneg  13126  pcmpt  13144  pcfac  13151  1arith  13168  setscomd  13444  ercpbllemg  13702  mgmidmo  13743  mgmlrid  13750  lidrideqd  13752  lidrididd  13753  grpinvalem  13756  grpinva  13757  issgrp  13769  isnsgrp  13772  sgrpass  13774  sgrp1  13777  issgrpd  13778  sgrppropd  13779  ismndd  13801  mndpropd  13804  imasmnd2  13810  mnd1  13813  mnd1id  13814  ismhm  13819  mhmpropd  13824  mhmlin  13825  mhmeql  13850  isgrp  13862  grppropd  13873  isgrpd2e  13876  dfgrp2  13883  isgrpid2  13896  grpidd2  13897  grpinvfvalg  13898  grpinvpropdg  13931  grpidssd  13932  grpinvssd  13933  grpsubrcan  13937  dfgrp3mlem  13954  grplactcnv  13958  imasgrp2  13964  mhmlem  13968  mulgnn0p1  13987  mulgaddcom  14000  mulginvcom  14001  mulgneg2  14010  mulgnnass  14011  mulgnn0ass  14012  mulgass  14013  mhmmulg  14017  isghm  14097  ghmlin  14102  ghmeql  14121  iscmn  14147  cmnpropd  14149  iscmnd  14152  cmnsubm  14163  abladdsub4  14169  imasabl  14191  gzsumconst  14194  gsummptfidmadd  14212  gsumconstcmn  14217  isrng  14284  rngass  14289  rngdi  14290  rngdir  14291  rngpropd  14305  imasrng  14306  issrg  14320  srgmulgass  14344  srgpcomp  14345  srg1expzeq1  14350  isring  14355  iscrng2  14370  ringpropd  14394  ringinvnz1ne0  14405  mulgass2  14414  ring1  14415  imasring  14420  opprnegg  14440  dvdsrd  14452  dvreq1  14500  rhmmul  14522  isrhm2d  14523  rhmopp  14534  rhmunitinv  14536  islring  14550  opprlring  14555  rrgval  14621  unitrrg  14627  opprdomnbg  14634  islmod  14678  lmodlema  14679  islmodd  14680  lmodvsmmulgdi  14711  lmodprop2d  14736  rmodislmodlem  14738  rmodislmod  14739  rnglidlmsgrp  14885  rnglidlrng  14886  quscrng  14921  cnfldmulg  14964  cnfldexp  14965  gsumfsum  14974  zndvds  15035  znf1o  15037  znunit  15045  isassa  15053  assalem  15054  isassad  15062  assapropd  15065  assamulgscm  15094  psr1clfi  15131  txcnp  15424  cnmpt11  15436  cnmpt21  15444  cnmptcom  15451  isxms  15604  xmspropd  15630  bdmopn  15657  dvexp  15864  dvmptfsum  15878  rpcxpmul2  16071  wilthlem1  16154  mpodvdsmulf1o  16206  fsumdvdsmul  16207  perfect  16223  lgsne0  16279  gausslemma2d  16310  lgseisenlem2  16312  lgsquad2lem2  16323  2lgslem1a  16329  2lgslem1b  16330  usgredg2v  16587  issubgr  16620  wkslem1  16683  wkslem2  16684  iswlk  16686  uspgr2wlkeq  16728  2wlklem  16739  wlkres  16742  eupth2lem3fi  16839  eupth2fi  16842  depindlem1  16869  depindlem2  16870  depindlem3  16871  depind  16872  nninffeq  17185