Theorem eqtr4di 2247

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
eqtr4di	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4di.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2200	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2245	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr4g  2254  rabxmdc  3483  relop  4817  csbcnvg  4851  dfiun3g  4924  dfiin3g  4925  resima2  4981  relcnvfld  5204  uniabio  5230  fntpg  5315  dffn5im  5609  dfimafn2  5613  fncnvima2  5686  fmptcof  5732  fcoconst  5736  fnasrng  5745  ffnov  6030  fnovim  6035  fnrnov  6073  foov  6074  funimassov  6077  ovelimab  6078  ofc12  6163  caofinvl  6165  dftpos3  6329  tfr0dm  6389  rdgisucinc  6452  oasuc  6531  ecinxp  6678  phplem1  6922  exmidpw  6978  exmidpweq  6979  unfiin  6996  fidcenumlemr  7030  0ct  7182  ctmlemr  7183  exmidaclem  7293  indpi  7428  nqnq0pi  7524  nq0m0r  7542  addnqpr1  7648  recexgt0sr  7859  suplocsrlempr  7893  recidpipr  7942  recidpirq  7944  axrnegex  7965  nntopi  7980  cnref1o  9744  fztp  10172  fseq1m1p1  10189  fz0to4untppr  10218  frecuzrdgrrn  10519  frecuzrdgsuc  10525  frecuzrdgsuctlem  10534  seq3val  10571  seqvalcd  10572  fser0const  10646  mulexpzap  10690  expaddzap  10694  bcp1m1  10876  iswrdiz  10961  cjexp  11077  rexuz3  11174  bdtri  11424  climconst  11474  sumfct  11558  zsumdc  11568  fsum3  11571  sum0  11572  fsumcnv  11621  mertenslem2  11720  zproddc  11763  fprodseq  11767  prod0  11769  prod1dc  11770  prodfct  11771  fprodcnv  11809  ef0lem  11844  efzval  11867  efival  11916  sinbnd  11936  cosbnd  11937  eucalgval  12249  eucalginv  12251  eucalglt  12252  eucalgcvga  12253  eucalg  12254  sqpweven  12370  2sqpwodd  12371  dfphi2  12415  phimullem  12420  prmdiv  12430  odzval  12437  pcval  12492  pczpre  12493  pcrec  12504  4sqlem17  12603  ennnfonelemhdmp1  12653  ennnfonelemkh  12656  ressinbasd  12779  restid2  12952  topnvalg  12955  prdsval  12977  prdsbas3  12991  pwsval  12995  pwsbas  12996  pwselbasb  12997  pwsplusgval  12999  pwsmulrval  13000  imasival  13010  imasplusg  13012  qusval  13027  xpsval  13056  ismgm  13061  plusffvalg  13066  grpidvalg  13077  igsumvalx  13093  issgrp  13107  ismnddef  13122  pws0g  13155  ismhm  13165  isgrp  13210  grpn0  13239  grpinvfvalg  13246  grpsubfvalg  13249  pwsinvg  13316  mulgfvalg  13329  mulgval  13330  mulgnn0p1  13341  issubg  13381  isnsg  13410  eqgfval  13430  quseccl0g  13439  isghm  13451  conjsubg  13485  conjsubgen  13486  iscmn  13501  mgpvalg  13557  isrng  13568  issrg  13599  isring  13634  iscrng  13637  opprvalg  13703  dfrhm2  13788  isnzr  13815  islring  13826  issubrg  13855  rrgval  13896  isdomn  13903  islmod  13925  scaffvalg  13940  lsssetm  13990  lspfval  14022  2idlval  14136  2idlvalg  14137  mulgrhm2  14244  zlmval  14261  znval  14270  znzrhfo  14282  znle2  14286  psrval  14300  mplvalcoe  14324  istps  14376  cldval  14443  ntrfval  14444  clsfval  14445  neifval  14484  restbasg  14512  tgrest  14513  txval  14599  upxp  14616  uptx  14618  txrest  14620  lmcn2  14624  cnmpt2t  14637  cnmpt2res  14641  imasnopn  14643  psmetxrge0  14676  xmetge0  14709  isxms  14795  isms  14797  bdxmet  14845  qtopbasss  14865  cnblcld  14879  mpomulcn  14910  negfcncf  14950  dvfvalap  15025  eldvap  15026  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvexp2  15056  dvrecap  15057  dveflem  15070  plyconst  15089  plycolemc  15102  sin0pilem1  15125  ptolemy  15168  coskpi  15192  logbrec  15304  mpodvdsmulf1o  15334  fsumdvdsmul  15335  lgslem1  15349  lgsval  15353  lgsval4  15369  lgsfcl3  15370  lgsdilem  15376  lgsdir2lem4  15380  lgsdir2lem5  15381  gausslemma2dlem5  15415  lgsquadlem2  15427  nninfsellemqall  15770