Theorem eqeq1d 2205

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq1d.1	|- ( ph -> A = B )

Assertion

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

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 |- ( ph -> A = B )
2		eqeq1 2203	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  rspcedeq1vd  2877  sbceq2g  3106  csbhypf  3123  csbiebt  3124  csbiebg  3127  dfss4st  3396  disjssun  3514  sneqrg  3792  preq12b  3800  preq12bg  3803  disji2  4026  iin0r  4202  opthg  4271  opeqsn  4285  unisucg  4449  opthreg  4592  tfisi  4623  dmsnopg  5141  relcoi1  5201  iotaeq  5227  iotabi  5228  fneq1  5346  fnun  5364  fnresdisj  5368  fnimadisj  5378  fnimaeq0  5379  sbcfng  5405  foeq1  5476  foco  5491  fveqeq2d  5566  fvelimab  5617  fvun1  5627  fvmptdv2  5651  fneqeql  5670  dffo3  5709  fvsng  5758  fconstfvm  5780  eufnfv  5793  f1veqaeq  5816  dff13f  5817  f1elima  5820  foeqcnvco  5837  f1eqcocnv  5838  acexmidlemab  5916  ovanraleqv  5946  eloprabga  6009  ovmpodv2  6056  ovi3  6060  ovelimab  6074  caovcang  6085  caovcan  6088  caovimo  6117  suppssfv  6131  suppssov1  6132  caofinvl  6160  uchoice  6195  op1stg  6208  op2ndg  6209  eqop  6235  reldm  6244  xporderlem  6289  tposfo2  6325  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  nnm0r  6537  nnmord  6575  nnaordex  6586  nnawordex  6587  ereq1  6599  eqerlem  6623  mapsn  6749  endisj  6883  pw2f1odclem  6895  xpf1o  6905  mapxpen  6909  fidifsnen  6931  supelti  7068  updjudhcoinlf  7146  updjudhcoinrg  7147  updjud  7148  omp1eomlem  7160  difinfsnlem  7165  nnnninfeq  7194  enomnilem  7204  finomni  7206  exmidomni  7208  fodjuomnilemres  7214  fodjuomni  7215  ismkvnex  7221  mkvprop  7224  fodjumkvlemres  7225  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemginf  7242  pm54.43  7257  exmidfodomrlemrALT  7270  cc2lem  7333  addnidpig  7403  ltexpi  7404  dfplpq2  7421  dfmpq2  7422  recexnq  7457  recmulnqg  7458  ltexnqq  7475  halfnqq  7477  enq0tr  7501  nqnq0pi  7505  addnnnq0  7516  addlocpr  7603  ltexprlemru  7679  ltexpri  7680  lteupri  7684  prplnqu  7687  recexpr  7705  addsrpr  7812  mulsrpr  7813  00sr  7836  negexsr  7839  recexgt0sr  7840  srpospr  7850  prsrriota  7855  caucvgsrlemfv  7858  map2psrprg  7872  elrealeu  7896  axrnegex  7946  axprecex  7947  rereceu  7956  recriota  7957  nntopi  7961  axcaucvglemval  7964  axcaucvglemcau  7965  cnegexlem1  8201  cnegex  8204  cnegex2  8205  subval  8218  subadd  8229  subadd2  8230  subsub23  8231  addsubeq4  8241  subcan2  8251  negcon1  8278  subcan  8281  addrsub  8397  ltadd2  8446  ltordlem  8509  recexre  8605  recexap  8680  muleqadd  8695  receuap  8696  divvalap  8701  divmulap  8702  rec11ap  8737  rerecapb  8870  zdiv  9414  uzin  9634  xaddval  9920  xnn0xadd0  9942  xnegdi  9943  xltadd1  9951  icc0r  10001  fznlem  10116  fseq1m1p1  10170  1fv  10214  fzon  10242  fvinim0ffz  10317  ioo0  10349  ico0  10351  ioc0  10352  flqbi  10380  divfl0  10386  modq0  10421  modqmuladdnn0  10460  addmodlteq  10490  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seq3f1olemstep  10606  seq3f1olemp  10607  seq3id  10617  seq3z  10620  qsqeqor  10742  mulreap  11029  rennim  11167  resqrexlemex  11190  rsqrmo  11192  resqrtcl  11194  rersqrtthlem  11195  sqrtsq2  11208  isumss  11556  fsum00  11627  telfsumo  11631  pwm1geoserap1  11673  prodssdc  11754  absefib  11936  efieq1re  11937  divides  11954  dvdsval2  11955  nndivides  11962  dvds0lem  11966  dvds1lem  11967  dvds2lem  11968  negdvdsb  11972  muldvds1  11981  muldvds2  11982  dvdscmulr  11985  dvdsmulcr  11986  dvdstr  11993  dvdsabseq  12012  divconjdvds  12014  odd2np1lem  12037  odd2np1  12038  even2n  12039  oddm1even  12040  2tp1odd  12049  opeo  12062  omeo  12063  m1exp1  12066  divalgb  12090  gcdaddm  12151  gcdabs1  12156  bezout  12178  gcdmultiple  12187  gcdmultiplez  12188  rplpwr  12194  rppwr  12195  nninfctlemfo  12207  alginv  12215  algcvga  12219  algfx  12220  eucalgval2  12221  coprmdvds  12260  qredeq  12264  qredeu  12265  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  rpexp  12321  rpexp12i  12323  cncongrprm  12325  qnumdenbi  12360  phival  12381  phicl2  12382  dfphi2  12388  phiprmpw  12390  phimullem  12393  eulerthlem1  12395  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlemth  12400  eulerth  12401  fermltl  12402  hashgcdlem  12406  phisum  12409  odzval  12410  odzdvds  12414  reumodprminv  12422  modprm0  12423  nnnn0modprm0  12424  modprmn0modprm0  12425  coprimeprodsq  12426  coprimeprodsq2  12427  pythagtriplem2  12435  pythagtrip  12452  pceulem  12463  pcval  12465  pcqmul  12472  pcqcl  12475  pcabs  12495  pc2dvds  12499  pcaddlem  12508  pcadd  12509  pcmpt  12512  prmpwdvds  12524  pockthi  12527  4sqlem12  12571  ennnfonelemhf1o  12630  fvprif  12986  mgmidmo  13015  grpidvalg  13016  grpidpropdg  13017  ismgmid  13020  ismgmid2  13023  mgmidsssn0  13027  grpinvalem  13028  grprida  13030  igsumvalx  13032  gsumress  13038  ismnddef  13059  sgrpidmndm  13061  ismndd  13078  mndpropd  13081  mndinvmod  13086  mnd1  13087  ismhm  13093  gsumvallem2  13125  grpinvex  13142  isgrpd2  13153  isgrpd  13155  dfgrp2  13159  grpinveu  13170  grpinvval  13175  grplinv  13182  isgrpinv  13186  grplrinv  13189  grpidinv2  13190  grpidinv  13191  grplmulf1o  13206  grpsubeq0  13218  grpsubadd  13220  dfgrp3mlem  13230  dfgrp3m  13231  grp1  13238  imasgrp2  13240  qusgrp2  13243  mhmmnd  13246  ghmgrp  13248  mulgval  13252  mulgaddcom  13276  eqg0el  13359  ghmeqker  13401  ghmf1  13403  conjnmzb  13410  ablsubadd  13442  ablsubsub23  13455  rngmneg1  13503  rngmneg2  13504  dfur2g  13518  srgideu  13528  srgidmlem  13534  issrgid  13537  srgrz  13540  srglz  13541  srgisid  13542  srg1zr  13543  ringideu  13573  ringidmlem  13578  isringid  13581  ringid  13582  qusring2  13622  oppr0g  13637  oppr1g  13638  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrmuld  13652  dvdsr01  13660  dvdsr02  13661  opprunitd  13666  crngunit  13667  unitinvinv  13680  dvreq1  13698  dvdsrpropdg  13703  rhmdvdsr  13731  lringuplu  13752  subrg1  13787  subrgdvds  13791  isrrg  13819  rrgeq0i  13820  rrgeq0  13821  domneq0  13828  islmod  13847  islmodd  13849  lmodprop2d  13904  lss1d  13939  cnfldui  14145  znval  14192  znidom  14213  znunit  14215  znrrg  14216  ntreq0  14368  ispsmet  14559  psmet0  14563  ismet  14580  isxmet  14581  xmeteq0  14595  metn0  14614  xmetres2  14615  xblss2ps  14640  xblss2  14641  xmseq0  14704  comet  14735  bdxmet  14737  cnmet  14766  ivthdec  14880  ivthreinc  14881  elply2  14971  reeff1o  15009  ioocosf1o  15090  logbgcd1irr  15203  logbgcd1irraplemexp  15204  mpodvdsmulf1o  15226  lgsval  15245  lgsdir  15276  lgsne0  15279  lgsprme0  15283  lgsdirnn0  15288  gausslemma2dlem0c  15292  gausslemma2dlem0i  15298  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  lgsquad3  15325  m1lgs  15326  2lgs  15345  2sqlem7  15362  2sqlem8  15364  2sqlem9  15365  bj-charfunbi  15457  pwle2  15643  subctctexmid  15645  peano4nninf  15650  nninfalllem1  15652  nninfsellemdc  15654  nninfsellemeq  15658  nninfsellemqall  15659  nninfsellemeqinf  15660  isomninnlem  15674  trilpolemlt1  15685  trirec0  15688  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  dceqnconst  15704  dcapnconst  15705