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	|- ( ph -> A = B )
eqeq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
eqeq12d	|- ( ph -> ( A = C <-> B = D ) )

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 |- ( ph -> A = B )
2		eqeq12d.2	. 2 |- ( ph -> C = D )
3		eqeq12 2251	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A = C <-> B = D ) )

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  10813  modqmul1  10829  addmodlteq  10850  frec2uzrdg  10861  frecuzrdgg  10868  seq3val  10912  seqvalcd  10913  seq3fveq2  10927  seqfveq2g  10929  seqfveqg  10930  seq3fveq  10931  seq3feq  10932  seq3shft2  10933  seqshft2g  10934  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqk  10959  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1olemp  10967  seq3f1oleml  10968  seqf1oglem2a  10970  seqf1oglem2  10972  seqf1og  10973  seq3id  10977  seq3id2  10978  seq3homo  10979  seqhomog  10982  seqfeq4g  10983  mulexp  11030  expadd  11033  expmul  11036  modqexp  11119  nn0opth2d  11177  bcpasc  11220  bcm1n  11223  hashennn  11235  hashen  11239  omgadd  11258  hashfzo  11279  hashfzp1  11281  hashxp  11283  hashmap  11284  hashfibclem  11298  hashfibc  11299  hashfacen  11300  hashf1lem1  11301  hashf1lem2  11302  hashf1  11303  seq3coll  11310  eqs1  11412  swrdspsleq  11455  pfxeq  11484  pfxsuff1eqwrdeq  11487  ccatopth2  11505  cats1un  11509  swrdccatin1  11513  swrdccat3blem  11527  shftvalg  11617  shftval4g  11618  replim  11640  cjreb  11647  cjexp  11674  absexp  11862  recan  11892  minclpr  12021  mingeb  12027  sumeq2  12144  zsumdc  12170  fsum3  12173  fsumf1o  12176  fsum3cvg2  12180  fsumadd  12192  isummulc2  12212  fsum2d  12221  fsummulc2  12234  fsumconst  12240  modfsummod  12244  fsumparts  12256  fsumrelem  12257  fsumiun  12263  binom  12270  bcxmas  12275  isumshft  12276  isumnn0nn  12279  mertenslem2  12322  clim2prod  12325  prodfrecap  12332  prodeq2  12343  zproddc  12365  fprodseq  12369  fprodf1o  12374  prodsnf  12378  fprodfac  12401  fprodabs  12402  fprodconst  12406  fprod2d  12409  fprodrec  12415  fprodmodd  12427  efne0  12464  efexp  12468  demoivreALT  12560  moddvds  12585  bitsinv1  12748  gcddiv  12815  alginv  12844  algfx  12849  lcmneg  12871  lcmid  12877  lcmgcdeq  12880  divgcdcoprm0  12898  cncongr1  12900  cncongr2  12901  nn0gcdsq  12999  crth  13025  eulerthlema  13031  eulerthlemh  13032  pythagtriplem1  13067  pcqmul  13105  pcexp  13111  pcneg  13127  pcmpt  13145  pcfac  13152  1arith  13169  setscomd  13445  ercpbllemg  13704  mgmidmo  13745  mgmlrid  13752  lidrideqd  13754  lidrididd  13755  grpinvalem  13758  grpinva  13759  issgrp  13771  isnsgrp  13774  sgrpass  13776  sgrp1  13779  issgrpd  13780  sgrppropd  13781  ismndd  13803  mndpropd  13806  imasmnd2  13812  mnd1  13815  mnd1id  13816  ismhm  13821  mhmpropd  13826  mhmlin  13827  mhmeql  13852  isgrp  13864  grppropd  13875  isgrpd2e  13878  dfgrp2  13885  isgrpid2  13898  grpidd2  13899  grpinvfvalg  13900  grpinvpropdg  13933  grpidssd  13934  grpinvssd  13935  grpsubrcan  13939  dfgrp3mlem  13956  grplactcnv  13960  imasgrp2  13966  mhmlem  13970  mulgnn0p1  13989  mulgaddcom  14002  mulginvcom  14003  mulgneg2  14012  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mhmmulg  14019  isghm  14099  ghmlin  14104  ghmeql  14123  cntzex  14144  cntzfval  14146  elcntz  14148  cntzsnval  14150  elcntzsn  14151  cntzi  14156  resscntz  14160  cntzmhm  14167  iscmn  14180  cmnpropd  14182  iscmnd  14185  cmnsubm  14196  abladdsub4  14202  imasabl  14224  gzsumconst  14227  gsummptfidmadd  14245  gsumconstcmn  14250  isrng  14317  rngass  14322  rngdi  14323  rngdir  14324  rngpropd  14338  imasrng  14339  issrg  14353  srgmulgass  14377  srgpcomp  14378  srg1expzeq1  14383  isring  14388  iscrng2  14403  ringpropd  14427  ringinvnz1ne0  14438  mulgass2  14447  ring1  14448  imasring  14453  opprnegg  14473  dvdsrd  14485  dvreq1  14533  rhmmul  14555  isrhm2d  14556  rhmopp  14567  rhmunitinv  14569  islring  14583  opprlring  14588  rrgval  14654  unitrrg  14660  opprdomnbg  14667  islmod  14711  lmodlema  14712  islmodd  14713  lmodvsmmulgdi  14744  lmodprop2d  14769  rmodislmodlem  14771  rmodislmod  14772  rnglidlmsgrp  14918  rnglidlrng  14919  quscrng  14954  cnfldmulg  14997  cnfldexp  14998  gsumfsum  15007  zndvds  15068  znf1o  15070  znunit  15078  isassa  15086  assalem  15087  isassad  15095  assapropd  15098  assamulgscm  15127  psr1clfi  15170  txcnp  15463  cnmpt11  15475  cnmpt21  15483  cnmptcom  15490  isxms  15643  xmspropd  15669  bdmopn  15696  dvexp  15903  dvmptfsum  15917  rpcxpmul2  16110  wilthlem1  16193  mpodvdsmulf1o  16245  fsumdvdsmul  16246  perfect  16262  lgsne0  16323  gausslemma2d  16354  lgseisenlem2  16356  lgsquad2lem2  16367  2lgslem1a  16373  2lgslem1b  16374  usgredg2v  16631  issubgr  16664  wkslem1  16727  wkslem2  16728  iswlk  16730  uspgr2wlkeq  16772  2wlklem  16783  wlkres  16786  eupth2lem3fi  16883  eupth2fi  16886  depindlem1  16913  depindlem2  16914  depindlem3  16915  depind  16916  nninffeq  17229