Theorem eqeq1d 2179

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

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq1d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq1 2177	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  rspcedeq1vd  2843  sbceq2g  3071  csbhypf  3087  csbiebt  3088  csbiebg  3091  dfss4st  3360  disjssun  3478  sneqrg  3749  preq12b  3757  preq12bg  3760  disji2  3982  iin0r  4155  opthg  4223  opeqsn  4237  unisucg  4399  opthreg  4540  tfisi  4571  dmsnopg  5082  relcoi1  5142  iotaeq  5168  iotabi  5169  fneq1  5286  fnun  5304  fnresdisj  5308  fnimadisj  5318  fnimaeq0  5319  sbcfng  5345  foeq1  5416  foco  5430  fveqeq2d  5504  fvelimab  5552  fvun1  5562  fvmptdv2  5585  fneqeql  5604  dffo3  5643  fvsng  5692  fconstfvm  5714  eufnfv  5726  f1veqaeq  5748  dff13f  5749  f1elima  5752  foeqcnvco  5769  f1eqcocnv  5770  acexmidlemab  5847  ovanraleqv  5877  eloprabga  5940  ovmpodv2  5986  ovi3  5989  ovelimab  6003  caovcang  6014  caovcan  6017  caovimo  6046  suppssfv  6057  suppssov1  6058  caofinvl  6083  op1stg  6129  op2ndg  6130  eqop  6156  reldm  6165  xporderlem  6210  tposfo2  6246  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  nnm0r  6458  nnmord  6496  nnaordex  6507  nnawordex  6508  ereq1  6520  eqerlem  6544  mapsn  6668  endisj  6802  xpf1o  6822  mapxpen  6826  fidifsnen  6848  supelti  6979  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  omp1eomlem  7071  difinfsnlem  7076  nnnninfeq  7104  enomnilem  7114  finomni  7116  exmidomni  7118  fodjuomnilemres  7124  fodjuomni  7125  ismkvnex  7131  mkvprop  7134  fodjumkvlemres  7135  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemginf  7152  pm54.43  7167  exmidfodomrlemrALT  7180  cc2lem  7228  addnidpig  7298  ltexpi  7299  dfplpq2  7316  dfmpq2  7317  recexnq  7352  recmulnqg  7353  ltexnqq  7370  halfnqq  7372  enq0tr  7396  nqnq0pi  7400  addnnnq0  7411  addlocpr  7498  ltexprlemru  7574  ltexpri  7575  lteupri  7579  prplnqu  7582  recexpr  7600  addsrpr  7707  mulsrpr  7708  00sr  7731  negexsr  7734  recexgt0sr  7735  srpospr  7745  prsrriota  7750  caucvgsrlemfv  7753  map2psrprg  7767  elrealeu  7791  axrnegex  7841  axprecex  7842  rereceu  7851  recriota  7852  nntopi  7856  axcaucvglemval  7859  axcaucvglemcau  7860  cnegexlem1  8094  cnegex  8097  cnegex2  8098  subval  8111  subadd  8122  subadd2  8123  subsub23  8124  addsubeq4  8134  subcan2  8144  negcon1  8171  subcan  8174  addrsub  8290  ltadd2  8338  ltordlem  8401  recexre  8497  recexap  8571  muleqadd  8586  receuap  8587  divvalap  8591  divmulap  8592  rec11ap  8627  zdiv  9300  uzin  9519  xaddval  9802  xnn0xadd0  9824  xnegdi  9825  xltadd1  9833  icc0r  9883  fznlem  9997  fseq1m1p1  10051  1fv  10095  fzon  10122  fvinim0ffz  10197  ioo0  10216  ico0  10218  ioc0  10219  flqbi  10246  divfl0  10252  modq0  10285  modqmuladdnn0  10324  addmodlteq  10354  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  seq3f1olemstep  10457  seq3f1olemp  10458  seq3id  10464  seq3z  10467  qsqeqor  10586  mulreap  10828  rennim  10966  resqrexlemex  10989  rsqrmo  10991  resqrtcl  10993  rersqrtthlem  10994  sqrtsq2  11007  isumss  11354  fsum00  11425  telfsumo  11429  pwm1geoserap1  11471  prodssdc  11552  absefib  11733  efieq1re  11734  divides  11751  dvdsval2  11752  nndivides  11759  dvds0lem  11763  dvds1lem  11764  dvds2lem  11765  negdvdsb  11769  muldvds1  11778  muldvds2  11779  dvdscmulr  11782  dvdsmulcr  11783  dvdstr  11790  dvdsabseq  11807  divconjdvds  11809  odd2np1lem  11831  odd2np1  11832  even2n  11833  oddm1even  11834  2tp1odd  11843  opeo  11856  omeo  11857  m1exp1  11860  divalgb  11884  gcdaddm  11939  gcdabs1  11944  bezout  11966  gcdmultiple  11975  gcdmultiplez  11976  rplpwr  11982  rppwr  11983  alginv  12001  algcvga  12005  algfx  12006  eucalgval2  12007  coprmdvds  12046  qredeq  12050  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  rpexp  12107  rpexp12i  12109  cncongrprm  12111  qnumdenbi  12146  phival  12167  phicl2  12168  dfphi2  12174  phiprmpw  12176  phimullem  12179  eulerthlem1  12181  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlemth  12186  eulerth  12187  fermltl  12188  hashgcdlem  12192  phisum  12194  odzval  12195  odzdvds  12199  reumodprminv  12207  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  coprimeprodsq  12211  coprimeprodsq2  12212  pythagtriplem2  12220  pythagtrip  12237  pceulem  12248  pcval  12250  pcqmul  12257  pcqcl  12260  pcabs  12279  pc2dvds  12283  pcaddlem  12292  pcadd  12293  pcmpt  12295  prmpwdvds  12307  pockthi  12310  ennnfonelemhf1o  12368  mgmidmo  12626  grpidvalg  12627  grpidpropdg  12628  ismgmid  12631  ismgmid2  12634  mgmidsssn0  12638  grprinvlem  12639  grpridd  12641  ismnddef  12654  sgrpidmndm  12656  ismndd  12673  mndpropd  12676  mndinvmod  12678  mnd1  12679  ismhm  12685  grpinvex  12718  isgrpd2  12727  isgrpd  12729  dfgrp2  12732  grpinveu  12741  grpinvval  12746  grplinv  12752  isgrpinv  12756  grplrinv  12757  grpidinv2  12758  grpidinv  12759  ntreq0  12926  ispsmet  13117  psmet0  13121  ismet  13138  isxmet  13139  xmeteq0  13153  metn0  13172  xmetres2  13173  xblss2ps  13198  xblss2  13199  xmseq0  13262  comet  13293  bdxmet  13295  cnmet  13324  ivthdec  13416  reeff1o  13488  ioocosf1o  13569  logbgcd1irr  13679  logbgcd1irraplemexp  13680  lgsval  13699  lgsdir  13730  lgsne0  13733  lgsprme0  13737  lgsdirnn0  13742  2sqlem7  13751  2sqlem8  13753  2sqlem9  13754  bj-charfunbi  13846  pwle2  14031  subctctexmid  14034  peano4nninf  14039  nninfalllem1  14041  nninfsellemdc  14043  nninfsellemeq  14047  nninfsellemqall  14048  nninfsellemeqinf  14049  isomninnlem  14062  trilpolemlt1  14073  trirec0  14076  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092