Theorem eqeq1d 2146

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 2144	. 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 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  rspcedeq1vd  2793  sbceq2g  3019  csbhypf  3033  csbiebt  3034  csbiebg  3037  dfss4st  3304  disjssun  3421  sneqrg  3684  preq12b  3692  preq12bg  3695  disji2  3917  iin0r  4088  opthg  4155  opeqsn  4169  unisucg  4331  opthreg  4466  tfisi  4496  dmsnopg  5005  relcoi1  5065  iotaeq  5091  iotabi  5092  fneq1  5206  fnun  5224  fnresdisj  5228  fnimadisj  5238  fnimaeq0  5239  sbcfng  5265  foeq1  5336  foco  5350  fveqeq2d  5422  fvelimab  5470  fvun1  5480  fvmptdv2  5503  fneqeql  5521  dffo3  5560  fvsng  5609  fconstfvm  5631  eufnfv  5641  f1veqaeq  5663  dff13f  5664  f1elima  5667  foeqcnvco  5684  f1eqcocnv  5685  acexmidlemab  5761  ovanraleqv  5791  eloprabga  5851  ovmpodv2  5897  ovi3  5900  ovelimab  5914  caovcang  5925  caovcan  5928  caovimo  5957  grprinvlem  5958  grpridd  5960  suppssfv  5971  suppssov1  5972  caofinvl  5997  op1stg  6041  op2ndg  6042  eqop  6068  reldm  6077  xporderlem  6121  tposfo2  6157  frec0g  6287  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecsuc  6297  nnm0r  6368  nnmord  6406  nnaordex  6416  nnawordex  6417  ereq1  6429  eqerlem  6453  mapsn  6577  endisj  6711  xpf1o  6731  mapxpen  6735  fidifsnen  6757  supelti  6882  updjudhcoinlf  6958  updjudhcoinrg  6959  updjud  6960  omp1eomlem  6972  difinfsnlem  6977  enomnilem  7003  finomni  7005  exmidomni  7007  fodjuomnilemres  7013  fodjuomni  7014  ismkvnex  7022  mkvprop  7025  fodjumkvlemres  7026  pm54.43  7039  exmidfodomrlemrALT  7052  addnidpig  7137  ltexpi  7138  dfplpq2  7155  dfmpq2  7156  recexnq  7191  recmulnqg  7192  ltexnqq  7209  halfnqq  7211  enq0tr  7235  nqnq0pi  7239  addnnnq0  7250  addlocpr  7337  ltexprlemru  7413  ltexpri  7414  lteupri  7418  prplnqu  7421  recexpr  7439  addsrpr  7546  mulsrpr  7547  00sr  7570  negexsr  7573  recexgt0sr  7574  srpospr  7584  prsrriota  7589  caucvgsrlemfv  7592  map2psrprg  7606  elrealeu  7630  axrnegex  7680  axprecex  7681  rereceu  7690  recriota  7691  nntopi  7695  axcaucvglemval  7698  axcaucvglemcau  7699  cnegexlem1  7930  cnegex  7933  cnegex2  7934  subval  7947  subadd  7958  subadd2  7959  subsub23  7960  addsubeq4  7970  subcan2  7980  negcon1  8007  subcan  8010  addrsub  8126  ltadd2  8174  ltordlem  8237  recexre  8333  recexap  8407  muleqadd  8422  receuap  8423  divvalap  8427  divmulap  8428  rec11ap  8463  zdiv  9132  uzin  9351  xaddval  9621  xnn0xadd0  9643  xnegdi  9644  xltadd1  9652  icc0r  9702  fznlem  9814  fseq1m1p1  9868  1fv  9909  fzon  9936  fvinim0ffz  10011  ioo0  10030  ico0  10032  ioc0  10033  flqbi  10056  divfl0  10062  modq0  10095  modqmuladdnn0  10134  addmodlteq  10164  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  seq3f1olemstep  10267  seq3f1olemp  10268  seq3id  10274  seq3z  10277  mulreap  10629  rennim  10767  resqrexlemex  10790  rsqrmo  10792  resqrtcl  10794  rersqrtthlem  10795  sqrtsq2  10808  isumss  11153  fsum00  11224  telfsumo  11228  pwm1geoserap1  11270  absefib  11466  efieq1re  11467  divides  11484  dvdsval2  11485  nndivides  11489  dvds0lem  11492  dvds1lem  11493  dvds2lem  11494  negdvdsb  11498  muldvds1  11507  muldvds2  11508  dvdscmulr  11511  dvdsmulcr  11512  dvdstr  11519  dvdsabseq  11534  divconjdvds  11536  odd2np1lem  11558  odd2np1  11559  even2n  11560  oddm1even  11561  2tp1odd  11570  opeo  11583  omeo  11584  m1exp1  11587  divalgb  11611  gcdaddm  11661  gcdabs1  11666  bezout  11688  gcdmultiple  11697  gcdmultiplez  11698  rplpwr  11704  rppwr  11705  alginv  11717  algcvga  11721  algfx  11722  eucalgval2  11723  coprmdvds  11762  qredeq  11766  qredeu  11767  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  rpexp  11820  rpexp12i  11822  cncongrprm  11824  qnumdenbi  11859  phival  11878  phicl2  11879  dfphi2  11885  phiprmpw  11887  phimullem  11890  hashgcdlem  11892  ennnfonelemhf1o  11915  ntreq0  12290  ispsmet  12481  psmet0  12485  ismet  12502  isxmet  12503  xmeteq0  12517  metn0  12536  xmetres2  12537  xblss2ps  12562  xblss2  12563  xmseq0  12626  comet  12657  bdxmet  12659  cnmet  12688  ivthdec  12780  pwle2  13182  subctctexmid  13185  peano4nninf  13189  nninfalllemn  13191  nninfalllem1  13192  nninfsellemdc  13195  nninfsellemeq  13199  nninfsellemqall  13200  nninfsellemeqinf  13201  nninfomnilem  13203  nninfomni  13204  isomninnlem  13214  trilpolemlt1  13223