Theorem eqtr2id 2786

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr2id.1	⊢ 𝐴 = 𝐵
eqtr2id.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtr2id	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2id

Step	Hyp	Ref	Expression
1		eqtr2id.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2id.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrid 2785	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2739	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqtr3di  2788  opeqsng  5504  relop  5851  ordintdif  6415  iotanul  6522  funopg  6583  funcnvres  6627  fpropnf1  7266  csbriota  7381  csbov123  7451  mpocurryd  8254  nneob  8655  sucdom2OLD  9082  pwfilem  9177  sucdom2  9206  unblem2  9296  pwfilemOLD  9346  pr2ne  9999  kmlem2  10146  kmlem11  10155  kmlem12  10156  cflim3  10257  1idsr  11093  recextlem1  11844  quoremz  13820  quoremnn0ALT  13822  intfrac2  13823  hashprg  14355  hashfacen  14413  hashfacenOLD  14414  leiso  14420  ccatrid  14537  repsw2  14901  repsw3  14902  cvgcmpce  15764  explecnv  15811  risefallfac  15968  ramub1lem1  16959  ressress  17193  subsubc  17803  grp1inv  18931  eqg0subg  19073  psgnunilem1  19361  psgn0fv0  19379  psgnsn  19388  efginvrel2  19595  efgredleme  19611  efgcpbllemb  19623  cmnbascntr  19673  frgpnabllem1  19741  gsumzaddlem  19789  gsumzmhm  19805  fsfnn0gsumfsffz  19851  dprd2da  19912  dpjcntz  19922  dpjdisj  19923  dpjlsm  19924  dpjidcl  19928  ablfac1lem  19938  ablfac1eu  19943  ringurd  20008  rnrhmsubrg  20352  lmhmlsp  20660  frlmip  21333  mplmon2mul  21630  1marepvmarrepid  22077  m1detdiag  22099  cramerimplem2  22186  pmatcollpw3lem  22285  chpscmatgsumbin  22346  chpscmatgsummon  22347  cayhamlem2  22386  neitr  22684  fixufil  23426  trust  23734  restmetu  24079  nmfval0  24099  nmval2  24101  rerest  24320  xrrest  24323  xrge0gsumle  24349  rrxip  24907  rrx0  24914  rrxdsfi  24928  voliunlem3  25069  volsup  25073  itg1addlem5  25218  itg2monolem1  25268  itg2cnlem2  25280  itgmpt  25300  iblcnlem1  25305  itgcnlem  25307  itgioo  25333  limcres  25403  mdegfval  25580  dgrlem  25743  coeidlem  25751  mcubic  26352  binom4  26355  dquartlem2  26357  amgm  26495  lgamgulmlem2  26534  eflgam  26549  wilthlem2  26573  rpvmasum2  27015  pntlemo  27110  bday0b  27332  wlkres  28958  3wlkond  29455  3cycld  29462  frgrncvvdeqlem3  29585  vc2OLD  29852  nvge0  29957  nmoo0  30075  bcsiALT  30463  pjchi  30716  shjshseli  30777  spanpr  30864  pjinvari  31475  mdslmd1lem2  31610  iundifdifd  31824  iundifdif  31825  fmptco1f1o  31888  gtiso  31953  gsumhashmul  32239  cycpmco2lem4  32319  cycpmconjslem2  32345  rspsnel  32515  qusima  32550  mxidlirred  32619  zarcls0  32879  esumpr2  33096  omssubaddlem  33329  eulerpartlemt  33401  ofcccat  33585  2cycld  34160  satfv1lem  34384  mpomulcn  35193  topjoin  35298  tailfval  35305  tailf  35308  dvasin  36620  dvacos  36621  opidon2OLD  36770  cdleme4  39157  cdleme22e  39263  cdleme22eALTN  39264  cdleme42a  39390  cdleme42d  39392  cdlemk20  39793  dih1dimatlem0  40247  lcfrlem2  40462  elrfi  41480  fzsplit1nn0  41540  rabdiophlem2  41588  eldioph4b  41597  diophren  41599  pell1qrgaplem  41659  rngunsnply  41963  om2  42203  oe2  42205  disjinfi  43939  fmuldfeq  44347  limciccioolb  44385  ditgeq3d  44728  stoweidlem44  44808  dirkertrigeq  44865  fourierdlem32  44903  fourierdlem33  44904  fourierdlem42  44913  fourierdlem62  44932  fourierdlem84  44954  fourierdlem85  44955  fourierdlem97  44967  fourierdlem98  44968  fourierdlem102  44972  fourierdlem104  44974  fourierdlem113  44983  fourierdlem114  44984  fourierswlem  44994  fouriersw  44995  sssalgen  45099  meadjun  45226  fcoreslem2  45822  fnfocofob  45835  deccarry  46067  fsumsplitsndif  46089  isomushgr  46542  ushrisomgr  46557  funcrngcsetcALT  46945  2sphere  47483  iscnrm3rlem1  47621