Theorem eqtr2id 2808

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqtr3di  2810  opeqsng  5474  relop  5827  cnvimassrndm  6078  ordintdif  6414  iotanul  6518  funopg  6575  funcnvres  6619  fpropnf1  7272  csbriota  7393  csbov123  7465  mpocurryd  8290  om2  8598  nneob  8669  sucdom2  9222  unblem2  9289  pwfilem  9313  prfi  9319  pr2ne  10088  kmlem2  10234  kmlem11  10243  kmlem12  10244  cflim3  10344  1idsr  11187  recextlem1  11950  quoremz  13999  quoremnn0ALT  14001  intfrac2  14002  hashprg  14543  hashfacen  14603  leiso  14608  ccatrid  14737  repsw2  15109  repsw3  15110  cvgcmpce  15991  explecnv  16040  risefallfac  16197  ramub1lem1  17210  ressress  17431  subsubc  18034  chnfi  18814  grp1inv  19264  eqg0subg  19417  psgnunilem1  19713  psgn0fv0  19731  psgnsn  19740  efginvrel2  19947  efgredleme  19963  efgcpbllemb  19975  cmnbascntr  20025  frgpnabllem1  20093  gsumzaddlem  20141  gsumzmhm  20157  fsfnn0gsumfsffz  20203  dprd2da  20264  dpjcntz  20274  dpjdisj  20275  dpjlsm  20276  dpjidcl  20280  ablfac1lem  20290  ablfac1eu  20295  ringurd  20417  funcrngcsetcALT  20899  lmhmlsp  21330  elrspsn  21531  frlmip  22090  opsrtoslem2  22371  mplmon2mul  22384  1marepvmarrepid  22896  m1detdiag  22918  cramerimplem2  23008  pmatcollpw3lem  23107  chpscmatgsumbin  23168  chpscmatgsummon  23169  cayhamlem2  23208  neitr  23504  fixufil  24247  trust  24554  restmetu  24895  nmfval0  24915  nmval2  24917  rerest  25129  xrrest  25133  xrge0gsumle  25159  mpomulcn  25194  rrxip  25717  rrx0  25724  rrxdsfi  25738  voliunlem3  25879  volsup  25883  itg1addlem5  26027  itg2monolem1  26077  itg2cnlem2  26089  itgmpt  26109  iblcnlem1  26114  itgcnlem  26116  itgioo  26142  limcres  26212  mdegfval  26386  dgrlem  26554  coeidlem  26562  mcubic  27181  binom4  27184  dquartlem2  27186  amgm  27324  lgamgulmlem2  27363  eflgam  27378  wilthlem2  27402  rpvmasum2  27845  pntlemo  27940  bday0b  28205  pw2cut2  28854  zz12s  28867  wlkres  30255  2cycld  30751  3wlkond  30778  3cycld  30785  frgrncvvdeqlem3  30908  vc2OLD  31176  nvge0  31281  nmoo0  31399  bcsiALT  31787  pjchi  32040  shjshseli  32101  spanpr  32188  pjinvari  32799  mdslmd1lem2  32934  iundifdifd  33204  iundifdif  33205  fresunsn  33267  fmptco1f1o  33275  gtiso  33342  gsumhashmul  33675  cycpmco2lem4  33737  cycpmconjslem2  33763  qusima  34006  mxidlirred  34044  selvascl  34196  esplyind  34254  vietalem  34258  extdgfialglem1  34371  2sqr3minply  34459  zarcls0  34547  esumpr2  34746  omssubaddlem  34978  eulerpartlemt  35050  ofcccat  35222  satfv1lem  36214  topjoin  37246  tailfval  37253  tailf  37256  dvasin  38716  dvacos  38717  opidon2OLD  38882  cdleme4  41389  cdleme22e  41495  cdleme22eALTN  41496  cdleme42a  41622  cdleme42d  41624  cdlemk20  42025  dih1dimatlem0  42479  lcfrlem2  42694  elrfi  43799  fzsplit1nn0  43859  rabdiophlem2  43903  eldioph4b  43912  diophren  43914  pell1qrgaplem  43974  rngunsnply  44265  oe2  44501  disjinfi  46301  fmuldfeq  46689  limciccioolb  46727  ditgeq3d  47068  stoweidlem44  47148  dirkertrigeq  47205  fourierdlem32  47243  fourierdlem33  47244  fourierdlem42  47253  fourierdlem62  47272  fourierdlem84  47294  fourierdlem85  47295  fourierdlem97  47307  fourierdlem98  47308  fourierdlem102  47312  fourierdlem104  47314  fourierdlem113  47323  fourierdlem114  47324  fourierswlem  47334  fouriersw  47335  sssalgen  47439  meadjun  47566  cos3t  48012  sin5tlem1  48013  fcoreslem2  48228  fnfocofob  48243  deccarry  48475  fsumsplitsndif  48545  gricushgr  49109  ushggricedg  49119  2sphere  49955  iscnrm3rlem1  50148