Theorem eqtr2d 2227

Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
eqtr2d	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2d

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2226	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2199	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1364

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-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186

This theorem is referenced by:  3eqtrrd  2231  3eqtr2rd  2233  ifandc  3596  ifordc  3597  onsucmin  4540  elxp4  5154  elxp5  5155  csbopeq1a  6243  ecinxp  6666  fundmen  6862  fidifsnen  6928  sbthlemi3  7020  ctm  7170  addpinq1  7526  1idsr  7830  prsradd  7848  cnegexlem3  8198  cnegex  8199  submul2  8420  mulsubfacd  8439  divadddivap  8748  infrenegsupex  9662  xadd4d  9954  fzval3  10274  fzoshftral  10308  ceiqm1l  10385  flqdiv  10395  flqmod  10412  intqfrac  10413  modqcyc2  10434  modqdi  10466  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seqf1oglem1  10593  seqf1oglem2  10594  seq3id2  10600  expnegzap  10647  binom2sub  10727  binom3  10731  fihashssdif  10892  reim  10999  mulreap  11011  addcj  11038  resqrexlemcalc1  11161  absimle  11231  infxrnegsupex  11409  clim2ser  11483  serf0  11498  summodclem3  11526  mptfzshft  11588  fsumrev  11589  fsum2mul  11599  isumsplit  11637  cvgratz  11678  mertenslemi1  11681  fprodrev  11765  ef4p  11840  tanval3ap  11860  efival  11878  sinmul  11890  divalglemnn  12062  dfgcd2  12154  lcmgcdlem  12218  lcm1  12222  oddpwdclemxy  12310  oddpwdclemdc  12314  eulerthlemth  12373  hashgcdeq  12380  powm2modprm  12393  pythagtriplem16  12420  pczpre  12438  pcqdiv  12448  pcadd  12481  pcfac  12491  4sqlem10  12528  4sqlem19  12550  ennnfonelemp1  12566  strslfvd  12663  xpsff1o  12935  gsumsplit1r  12984  grpinvssd  13152  grpinvval2  13158  gsumfzreidx  13410  opprrngbg  13577  opprringbg  13579  ringinvdv  13644  lss1d  13882  znzrh2  14145  cnclima  14402  divcncfap  14793  dveflem  14905  plycjlemc  14938  tangtx  15014  abssinper  15022  reexplog  15047  rprelogbdiv  15130  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  lgseisenlem2  15228  lgsquadlem1  15234  2sqlem2  15272  mul2sq  15273