Theorem eqtr2id 2777

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 2776	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2735	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqtr3di  2779  opeqsng  5463  relop  5814  ordintdif  6383  iotanul  6489  funopg  6550  funcnvres  6594  fpropnf1  7242  csbriota  7359  csbov123  7431  mpocurryd  8248  nneob  8620  sucdom2  9167  unblem2  9240  pwfilem  9267  prfi  9274  pr2ne  9957  kmlem2  10105  kmlem11  10114  kmlem12  10115  cflim3  10215  1idsr  11051  recextlem1  11808  quoremz  13817  quoremnn0ALT  13819  intfrac2  13820  hashprg  14360  hashfacen  14419  leiso  14424  ccatrid  14552  repsw2  14916  repsw3  14917  cvgcmpce  15784  explecnv  15831  risefallfac  15990  ramub1lem1  16997  ressress  17217  subsubc  17815  grp1inv  18980  eqg0subg  19128  psgnunilem1  19423  psgn0fv0  19441  psgnsn  19450  efginvrel2  19657  efgredleme  19673  efgcpbllemb  19685  cmnbascntr  19735  frgpnabllem1  19803  gsumzaddlem  19851  gsumzmhm  19867  fsfnn0gsumfsffz  19913  dprd2da  19974  dpjcntz  19984  dpjdisj  19985  dpjlsm  19986  dpjidcl  19990  ablfac1lem  20000  ablfac1eu  20005  ringurd  20094  funcrngcsetcALT  20550  lmhmlsp  20956  elrspsn  21150  frlmip  21687  opsrtoslem2  21963  mplmon2mul  21976  1marepvmarrepid  22462  m1detdiag  22484  cramerimplem2  22571  pmatcollpw3lem  22670  chpscmatgsumbin  22731  chpscmatgsummon  22732  cayhamlem2  22771  neitr  23067  fixufil  23809  trust  24117  restmetu  24458  nmfval0  24478  nmval2  24480  rerest  24692  xrrest  24696  xrge0gsumle  24722  mpomulcn  24758  rrxip  25290  rrx0  25297  rrxdsfi  25311  voliunlem3  25453  volsup  25457  itg1addlem5  25601  itg2monolem1  25651  itg2cnlem2  25663  itgmpt  25684  iblcnlem1  25689  itgcnlem  25691  itgioo  25717  limcres  25787  mdegfval  25967  dgrlem  26134  coeidlem  26142  mcubic  26757  binom4  26760  dquartlem2  26762  amgm  26901  lgamgulmlem2  26940  eflgam  26955  wilthlem2  26979  rpvmasum2  27423  pntlemo  27518  bday0b  27742  zzs12  28339  wlkres  29598  3wlkond  30100  3cycld  30107  frgrncvvdeqlem3  30230  vc2OLD  30497  nvge0  30602  nmoo0  30720  bcsiALT  31108  pjchi  31361  shjshseli  31422  spanpr  31509  pjinvari  32120  mdslmd1lem2  32255  iundifdifd  32490  iundifdif  32491  fmptco1f1o  32557  gtiso  32624  gsumhashmul  33001  cycpmco2lem4  33086  cycpmconjslem2  33112  qusima  33379  mxidlirred  33443  2sqr3minply  33770  zarcls0  33858  esumpr2  34057  omssubaddlem  34290  eulerpartlemt  34362  ofcccat  34534  2cycld  35125  satfv1lem  35349  topjoin  36353  tailfval  36360  tailf  36363  dvasin  37698  dvacos  37699  opidon2OLD  37848  cdleme4  40232  cdleme22e  40338  cdleme22eALTN  40339  cdleme42a  40465  cdleme42d  40467  cdlemk20  40868  dih1dimatlem0  41322  lcfrlem2  41537  elrfi  42682  fzsplit1nn0  42742  rabdiophlem2  42790  eldioph4b  42799  diophren  42801  pell1qrgaplem  42861  rngunsnply  43158  om2  43393  oe2  43395  disjinfi  45186  fmuldfeq  45581  limciccioolb  45619  ditgeq3d  45962  stoweidlem44  46042  dirkertrigeq  46099  fourierdlem32  46137  fourierdlem33  46138  fourierdlem42  46147  fourierdlem62  46166  fourierdlem84  46188  fourierdlem85  46189  fourierdlem97  46201  fourierdlem98  46202  fourierdlem102  46206  fourierdlem104  46208  fourierdlem113  46217  fourierdlem114  46218  fourierswlem  46228  fouriersw  46229  sssalgen  46333  meadjun  46460  fcoreslem2  47065  fnfocofob  47080  deccarry  47312  fsumsplitsndif  47374  gricushgr  47917  ushggricedg  47927  2sphere  48738  iscnrm3rlem1  48928