Theorem eqtr2d 2204

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  3eqtrrd  2208  3eqtr2rd  2210  ifandc  3562  onsucmin  4489  elxp4  5096  elxp5  5097  csbopeq1a  6164  ecinxp  6584  fundmen  6780  fidifsnen  6844  sbthlemi3  6932  ctm  7082  addpinq1  7413  1idsr  7717  prsradd  7735  cnegexlem3  8083  cnegex  8084  submul2  8305  mulsubfacd  8324  divadddivap  8631  infrenegsupex  9540  xadd4d  9829  fzval3  10147  fzoshftral  10181  ceiqm1l  10254  flqdiv  10264  flqmod  10281  intqfrac  10282  modqcyc2  10303  modqdi  10335  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  seq3id2  10452  expnegzap  10497  binom2sub  10576  binom3  10580  fihashssdif  10740  reim  10803  mulreap  10815  addcj  10842  resqrexlemcalc1  10965  absimle  11035  infxrnegsupex  11213  clim2ser  11287  serf0  11302  summodclem3  11330  mptfzshft  11392  fsumrev  11393  fsum2mul  11403  isumsplit  11441  cvgratz  11482  mertenslemi1  11485  fprodrev  11569  ef4p  11644  tanval3ap  11664  efival  11682  sinmul  11694  divalglemnn  11864  dfgcd2  11956  lcmgcdlem  12018  lcm1  12022  oddpwdclemxy  12110  oddpwdclemdc  12114  eulerthlemth  12173  hashgcdeq  12180  powm2modprm  12193  pythagtriplem16  12220  pczpre  12238  pcqdiv  12248  pcadd  12280  pcfac  12289  4sqlem10  12326  ennnfonelemp1  12348  strslfvd  12444  cnclima  12938  dveflem  13402  tangtx  13474  abssinper  13482  reexplog  13507  rprelogbdiv  13590  lgsdirnn0  13663  lgsdinn0  13664  2sqlem2  13666  mul2sq  13667