Theorem eqeq12d 2102

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 2100	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  cdeqeq  2833  sbceqg  2945  csbing  3205  uniprg  3663  unisng  3665  intprg  3716  iununir  3807  csbopabg  3908  undifexmid  4019  exmidundif  4026  limeq  4195  onsucuni2  4370  ordpwsucexmid  4376  csbima12g  4780  dmsnsnsng  4895  cnvsng  4903  csbiotag  4995  fvmptf  5379  eqfnfv2f  5385  fvreseq  5387  fmptco  5448  fnressn  5467  fvsng  5477  cocan1  5548  cocan2  5549  fliftfun  5557  csbriotag  5602  csbov123g  5669  eqfnov  5733  ovmpt2s  5750  ov2gf  5751  ovmpt2dxf  5752  caovcomg  5782  caovassg  5785  caovcang  5788  caovcanrd  5790  caovcan  5791  caovdig  5801  caovdirg  5804  caovimo  5820  grprinvlem  5821  grprinvd  5822  offveqb  5856  op1stg  5903  op2ndg  5904  f1o2ndf1  5975  tfrlem1  6055  tfrlem3ag  6056  tfrlem3a  6057  tfrlem5  6061  tfrlem9  6066  tfr0dm  6069  tfrlemiubacc  6077  tfrlemiex  6078  tfrlemi1  6079  tfr1onlem3ag  6084  tfr1onlemubacc  6093  tfr1onlemex  6094  tfr1onlemaccex  6095  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllemubacc  6106  tfrcllemex  6107  tfrcllemaccex  6108  tfrcllemres  6109  tfrcldm  6110  tfri3  6114  rdg0g  6135  frecrdg  6155  nna0r  6221  nnacom  6227  nnaass  6228  nndi  6229  nnmass  6230  nnmsucr  6231  nnmcom  6232  ecopovtrn  6369  ecopovsymg  6371  ecopovtrng  6372  ecovcom  6379  ecovicom  6380  ecovass  6381  ecoviass  6382  ecovdi  6383  ecovidi  6384  dom2lem  6469  ordiso2  6707  updjud  6752  exmidfodomrlemrALT  6808  addcanpig  6872  mulcanpig  6873  mulcmpblnq  6906  mulpipqqs  6911  ordpipqqs  6912  mulidnq  6927  enq0sym  6970  nqnq0  6979  mulcmpblnq0  6982  distrnq0  6997  mulcomnq0  6998  addassnq0  7000  nq02m  7003  genipv  7047  cauappcvgprlemladd  7196  addcmpblnr  7264  0idsr  7292  1idsr  7293  axaddcom  7384  ax1rid  7391  ax0id  7392  rereceu  7403  axcaucvg  7414  mulid1  7464  readdcan  7601  cnegexlem1  7636  cnegexlem3  7638  addcan  7641  addcan2  7642  apti  8075  mulcanapd  8104  mulcanap2d  8105  div11ap  8141  divmuleqap  8158  conjmulap  8170  eqneg  8173  cnref1o  9102  fzsuc2  9460  fzprval  9463  fztpval  9464  qtri3or  9619  modqadd1  9733  modqmul1  9749  addmodlteq  9770  frec2uzrdg  9781  frecuzrdgg  9788  iseqvalt  9838  seq3val  9839  iseqoveq  9850  iseqsst  9851  iseqfveq2  9855  seq3fveq2  9857  iseqfveq  9859  seq3fveq  9860  iseqfeq  9861  seq3feq  9862  iseqshft2  9863  seq3split  9872  iseqsplit  9873  iseqcaopr3  9875  iseqcaopr2  9876  iseqf1olemkle  9878  iseqf1olemklt  9879  iseqf1olemqk  9888  seq3f1olemqsum  9894  seq3f1olemstep  9895  seq3f1olemp  9896  seq3f1oleml  9897  iseqid  9904  seq3id2  9905  iseqid2  9906  iseqhomo  9907  seq3homo  9909  mulexp  9959  expadd  9962  expmul  9965  nn0opth2d  10096  bcpasc  10139  hashennn  10153  hashen  10157  omgadd  10175  hashfzo  10195  hashfzp1  10197  hashxp  10199  hashfacen  10206  iseqcoll  10212  shftvalg  10235  shftval4g  10236  replim  10258  cjreb  10265  cjexp  10292  absexp  10477  recan  10507  sumeq2  10712  zisum  10738  fisum  10742  fsumf1o  10746  fisumcvg2  10750  fsumadd  10763  isummulc2  10783  fsum2d  10792  fsummulc2  10805  fsumconst  10811  modfsummod  10815  fsumparts  10827  fsumrelem  10828  fsumiun  10833  binom  10840  bcxmas  10845  isumshft  10846  isumnn0nn  10849  moddvds  10898  gcddiv  11101  ialginv  11122  ialgfx  11127  lcmneg  11149  lcmid  11155  lcmgcdeq  11158  divgcdcoprm0  11176  cncongr1  11178  cncongr2  11179  nn0gcdsq  11271  crth  11293  nninfalllemn  11555