Theorem eqtr2id 2781

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  eqtr3di  2783  opeqsng  5446  relop  5794  ordintdif  6362  iotanul  6466  funopg  6520  funcnvres  6564  fpropnf1  7207  csbriota  7324  csbov123  7396  mpocurryd  8205  nneob  8577  sucdom2  9119  unblem2  9184  pwfilem  9209  prfi  9215  pr2ne  9903  kmlem2  10050  kmlem11  10059  kmlem12  10060  cflim3  10160  1idsr  10996  recextlem1  11754  quoremz  13761  quoremnn0ALT  13763  intfrac2  13764  hashprg  14304  hashfacen  14363  leiso  14368  ccatrid  14497  repsw2  14859  repsw3  14860  cvgcmpce  15727  explecnv  15774  risefallfac  15933  ramub1lem1  16940  ressress  17160  subsubc  17762  chnfi  18542  grp1inv  18963  eqg0subg  19110  psgnunilem1  19407  psgn0fv0  19425  psgnsn  19434  efginvrel2  19641  efgredleme  19657  efgcpbllemb  19669  cmnbascntr  19719  frgpnabllem1  19787  gsumzaddlem  19835  gsumzmhm  19851  fsfnn0gsumfsffz  19897  dprd2da  19958  dpjcntz  19968  dpjdisj  19969  dpjlsm  19970  dpjidcl  19974  ablfac1lem  19984  ablfac1eu  19989  ringurd  20105  funcrngcsetcALT  20558  lmhmlsp  20985  elrspsn  21179  frlmip  21717  opsrtoslem2  21992  mplmon2mul  22005  1marepvmarrepid  22491  m1detdiag  22513  cramerimplem2  22600  pmatcollpw3lem  22699  chpscmatgsumbin  22760  chpscmatgsummon  22761  cayhamlem2  22800  neitr  23096  fixufil  23838  trust  24145  restmetu  24486  nmfval0  24506  nmval2  24508  rerest  24720  xrrest  24724  xrge0gsumle  24750  mpomulcn  24786  rrxip  25318  rrx0  25325  rrxdsfi  25339  voliunlem3  25481  volsup  25485  itg1addlem5  25629  itg2monolem1  25679  itg2cnlem2  25691  itgmpt  25712  iblcnlem1  25717  itgcnlem  25719  itgioo  25745  limcres  25815  mdegfval  25995  dgrlem  26162  coeidlem  26170  mcubic  26785  binom4  26788  dquartlem2  26790  amgm  26929  lgamgulmlem2  26968  eflgam  26983  wilthlem2  27007  rpvmasum2  27451  pntlemo  27546  bday0b  27775  pw2cut2  28383  zzs12  28386  wlkres  29649  3wlkond  30153  3cycld  30160  frgrncvvdeqlem3  30283  vc2OLD  30550  nvge0  30655  nmoo0  30773  bcsiALT  31161  pjchi  31414  shjshseli  31475  spanpr  31562  pjinvari  32173  mdslmd1lem2  32308  iundifdifd  32543  iundifdif  32544  fmptco1f1o  32617  gtiso  32686  gsumhashmul  33048  cycpmco2lem4  33105  cycpmconjslem2  33131  qusima  33380  mxidlirred  33444  esplyind  33613  extdgfialglem1  33726  2sqr3minply  33814  zarcls0  33902  esumpr2  34101  omssubaddlem  34333  eulerpartlemt  34405  ofcccat  34577  2cycld  35203  satfv1lem  35427  topjoin  36430  tailfval  36437  tailf  36440  dvasin  37765  dvacos  37766  opidon2OLD  37915  cdleme4  40358  cdleme22e  40464  cdleme22eALTN  40465  cdleme42a  40591  cdleme42d  40593  cdlemk20  40994  dih1dimatlem0  41448  lcfrlem2  41663  elrfi  42812  fzsplit1nn0  42872  rabdiophlem2  42920  eldioph4b  42929  diophren  42931  pell1qrgaplem  42991  rngunsnply  43287  om2  43522  oe2  43524  disjinfi  45314  fmuldfeq  45708  limciccioolb  45746  ditgeq3d  46087  stoweidlem44  46167  dirkertrigeq  46224  fourierdlem32  46262  fourierdlem33  46263  fourierdlem42  46272  fourierdlem62  46291  fourierdlem84  46313  fourierdlem85  46314  fourierdlem97  46326  fourierdlem98  46327  fourierdlem102  46331  fourierdlem104  46333  fourierdlem113  46342  fourierdlem114  46343  fourierswlem  46353  fouriersw  46354  sssalgen  46458  meadjun  46585  fcoreslem2  47189  fnfocofob  47204  deccarry  47436  fsumsplitsndif  47498  gricushgr  48042  ushggricedg  48052  2sphere  48875  iscnrm3rlem1  49065