Theorem eqeq1d 2174

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 2172	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  rspcedeq1vd  2838  sbceq2g  3066  csbhypf  3082  csbiebt  3083  csbiebg  3086  dfss4st  3354  disjssun  3471  sneqrg  3741  preq12b  3749  preq12bg  3752  disji2  3974  iin0r  4147  opthg  4215  opeqsn  4229  unisucg  4391  opthreg  4532  tfisi  4563  dmsnopg  5074  relcoi1  5134  iotaeq  5160  iotabi  5161  fneq1  5275  fnun  5293  fnresdisj  5297  fnimadisj  5307  fnimaeq0  5308  sbcfng  5334  foeq1  5405  foco  5419  fveqeq2d  5493  fvelimab  5541  fvun1  5551  fvmptdv2  5574  fneqeql  5592  dffo3  5631  fvsng  5680  fconstfvm  5702  eufnfv  5714  f1veqaeq  5736  dff13f  5737  f1elima  5740  foeqcnvco  5757  f1eqcocnv  5758  acexmidlemab  5835  ovanraleqv  5865  eloprabga  5925  ovmpodv2  5971  ovi3  5974  ovelimab  5988  caovcang  5999  caovcan  6002  caovimo  6031  grprinvlem  6032  grpridd  6034  suppssfv  6045  suppssov1  6046  caofinvl  6071  op1stg  6115  op2ndg  6116  eqop  6142  reldm  6151  xporderlem  6195  tposfo2  6231  frec0g  6361  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  nnm0r  6443  nnmord  6481  nnaordex  6491  nnawordex  6492  ereq1  6504  eqerlem  6528  mapsn  6652  endisj  6786  xpf1o  6806  mapxpen  6810  fidifsnen  6832  supelti  6963  updjudhcoinlf  7041  updjudhcoinrg  7042  updjud  7043  omp1eomlem  7055  difinfsnlem  7060  nnnninfeq  7088  enomnilem  7098  finomni  7100  exmidomni  7102  fodjuomnilemres  7108  fodjuomni  7109  ismkvnex  7115  mkvprop  7118  fodjumkvlemres  7119  enmkvlem  7121  enwomnilem  7129  pm54.43  7142  exmidfodomrlemrALT  7155  cc2lem  7203  addnidpig  7273  ltexpi  7274  dfplpq2  7291  dfmpq2  7292  recexnq  7327  recmulnqg  7328  ltexnqq  7345  halfnqq  7347  enq0tr  7371  nqnq0pi  7375  addnnnq0  7386  addlocpr  7473  ltexprlemru  7549  ltexpri  7550  lteupri  7554  prplnqu  7557  recexpr  7575  addsrpr  7682  mulsrpr  7683  00sr  7706  negexsr  7709  recexgt0sr  7710  srpospr  7720  prsrriota  7725  caucvgsrlemfv  7728  map2psrprg  7742  elrealeu  7766  axrnegex  7816  axprecex  7817  rereceu  7826  recriota  7827  nntopi  7831  axcaucvglemval  7834  axcaucvglemcau  7835  cnegexlem1  8069  cnegex  8072  cnegex2  8073  subval  8086  subadd  8097  subadd2  8098  subsub23  8099  addsubeq4  8109  subcan2  8119  negcon1  8146  subcan  8149  addrsub  8265  ltadd2  8313  ltordlem  8376  recexre  8472  recexap  8546  muleqadd  8561  receuap  8562  divvalap  8566  divmulap  8567  rec11ap  8602  zdiv  9275  uzin  9494  xaddval  9777  xnn0xadd0  9799  xnegdi  9800  xltadd1  9808  icc0r  9858  fznlem  9972  fseq1m1p1  10026  1fv  10070  fzon  10097  fvinim0ffz  10172  ioo0  10191  ico0  10193  ioc0  10194  flqbi  10221  divfl0  10227  modq0  10260  modqmuladdnn0  10299  addmodlteq  10329  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  seq3f1olemstep  10432  seq3f1olemp  10433  seq3id  10439  seq3z  10442  qsqeqor  10561  mulreap  10802  rennim  10940  resqrexlemex  10963  rsqrmo  10965  resqrtcl  10967  rersqrtthlem  10968  sqrtsq2  10981  isumss  11328  fsum00  11399  telfsumo  11403  pwm1geoserap1  11445  prodssdc  11526  absefib  11707  efieq1re  11708  divides  11725  dvdsval2  11726  nndivides  11733  dvds0lem  11737  dvds1lem  11738  dvds2lem  11739  negdvdsb  11743  muldvds1  11752  muldvds2  11753  dvdscmulr  11756  dvdsmulcr  11757  dvdstr  11764  dvdsabseq  11781  divconjdvds  11783  odd2np1lem  11805  odd2np1  11806  even2n  11807  oddm1even  11808  2tp1odd  11817  opeo  11830  omeo  11831  m1exp1  11834  divalgb  11858  gcdaddm  11913  gcdabs1  11918  bezout  11940  gcdmultiple  11949  gcdmultiplez  11950  rplpwr  11956  rppwr  11957  alginv  11975  algcvga  11979  algfx  11980  eucalgval2  11981  coprmdvds  12020  qredeq  12024  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  rpexp  12081  rpexp12i  12083  cncongrprm  12085  qnumdenbi  12120  phival  12141  phicl2  12142  dfphi2  12148  phiprmpw  12150  phimullem  12153  eulerthlem1  12155  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlemth  12160  eulerth  12161  fermltl  12162  hashgcdlem  12166  phisum  12168  odzval  12169  odzdvds  12173  reumodprminv  12181  modprm0  12182  nnnn0modprm0  12183  modprmn0modprm0  12184  coprimeprodsq  12185  coprimeprodsq2  12186  pythagtriplem2  12194  pythagtrip  12211  pceulem  12222  pcval  12224  pcqmul  12231  pcqcl  12234  pcabs  12253  pc2dvds  12257  pcaddlem  12266  pcadd  12267  pcmpt  12269  prmpwdvds  12281  pockthi  12284  ennnfonelemhf1o  12342  ntreq0  12732  ispsmet  12923  psmet0  12927  ismet  12944  isxmet  12945  xmeteq0  12959  metn0  12978  xmetres2  12979  xblss2ps  13004  xblss2  13005  xmseq0  13068  comet  13099  bdxmet  13101  cnmet  13130  ivthdec  13222  reeff1o  13294  ioocosf1o  13375  logbgcd1irr  13485  logbgcd1irraplemexp  13486  lgsval  13505  lgsdir  13536  lgsne0  13539  lgsprme0  13543  lgsdirnn0  13548  2sqlem7  13557  2sqlem8  13559  2sqlem9  13560  bj-charfunbi  13653  pwle2  13838  subctctexmid  13841  peano4nninf  13846  nninfalllem1  13848  nninfsellemdc  13850  nninfsellemeq  13854  nninfsellemqall  13855  nninfsellemeqinf  13856  isomninnlem  13869  trilpolemlt1  13880  trirec0  13883  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891  dceqnconst  13898  dcapnconst  13899