Theorem eceq1d 6655

Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)

Hypothesis

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

Assertion

Ref	Expression
eceq1d	|- ( ph -> [ A ] C = [ B ] C )

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 |- ( ph -> A = B )
2		eceq1 6654	. 2 |- ( A = B -> [ A ] C = [ B ] C )
3	1, 2	syl 14	1 |- ( ph -> [ A ] C = [ B ] C )

Syntax hints:   -> wi 4   = wceq 1372   [cec 6617

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-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044  df-opab 4105  df-xp 4680  df-cnv 4682  df-dm 4684  df-rn 4685  df-res 4686  df-ima 4687  df-ec 6621

This theorem is referenced by:  brecop  6711  eroveu  6712  th3qlem1  6723  th3qlem2  6724  th3q  6726  oviec  6727  ecovcom  6728  ecovicom  6729  ecovass  6730  ecoviass  6731  ecovdi  6732  ecovidi  6733  mulidnq  7501  recexnq  7502  ltexnqq  7520  archnqq  7529  prarloclemarch2  7531  addnq0mo  7559  mulnq0mo  7560  addnnnq0  7561  mulnnnq0  7562  nqnq0a  7566  nqnq0m  7567  nq0a0  7569  nnanq0  7570  distrnq0  7571  mulcomnq0  7572  addassnq0  7574  addpinq1  7576  nq02m  7577  prarloclemlo  7606  prarloclem3  7609  prarloclem5  7612  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  addsrmo  7855  mulsrmo  7856  addsrpr  7857  mulsrpr  7858  prsrriota  7900  caucvgsrlemfv  7903  caucvgsr  7914  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  suplocsr  7921  pitonnlem2  7959  pitonn  7960  nntopi  8006  axcaucvglemval  8009  qus0  13513  qusinv  13514  qussub  13515  quscrng  14237