Theorem eqtr4di 2228

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 2181	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2226	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr4g  2235  rabxmdc  3456  relop  4779  csbcnvg  4813  dfiun3g  4886  dfiin3g  4887  resima2  4943  relcnvfld  5164  uniabio  5190  fntpg  5274  dffn5im  5563  dfimafn2  5567  fncnvima2  5639  fmptcof  5685  fcoconst  5689  fnasrng  5698  ffnov  5981  fnovim  5985  fnrnov  6022  foov  6023  funimassov  6026  ovelimab  6027  ofc12  6105  caofinvl  6107  dftpos3  6265  tfr0dm  6325  rdgisucinc  6388  oasuc  6467  ecinxp  6612  phplem1  6854  exmidpw  6910  exmidpweq  6911  unfiin  6927  fidcenumlemr  6956  0ct  7108  ctmlemr  7109  exmidaclem  7209  indpi  7343  nqnq0pi  7439  nq0m0r  7457  addnqpr1  7563  recexgt0sr  7774  suplocsrlempr  7808  recidpipr  7857  recidpirq  7859  axrnegex  7880  nntopi  7895  cnref1o  9652  fztp  10080  fseq1m1p1  10097  fz0to4untppr  10126  frecuzrdgrrn  10410  frecuzrdgsuc  10416  frecuzrdgsuctlem  10425  seq3val  10460  seqvalcd  10461  fser0const  10518  mulexpzap  10562  expaddzap  10566  bcp1m1  10747  cjexp  10904  rexuz3  11001  bdtri  11250  climconst  11300  sumfct  11384  zsumdc  11394  fsum3  11397  sum0  11398  fsumcnv  11447  mertenslem2  11546  zproddc  11589  fprodseq  11593  prod0  11595  prod1dc  11596  prodfct  11597  fprodcnv  11635  ef0lem  11670  efzval  11693  efival  11742  sinbnd  11762  cosbnd  11763  eucalgval  12056  eucalginv  12058  eucalglt  12059  eucalgcvga  12060  eucalg  12061  sqpweven  12177  2sqpwodd  12178  dfphi2  12222  phimullem  12227  prmdiv  12237  odzval  12243  pcval  12298  pczpre  12299  pcrec  12310  ennnfonelemhdmp1  12412  ennnfonelemkh  12415  ressinbasd  12535  topnvalg  12705  imasival  12732  imasplusg  12734  qusval  12749  xpsval  12776  ismgm  12781  plusffvalg  12786  grpidvalg  12797  issgrp  12814  ismnddef  12824  ismhm  12858  isgrp  12888  grpn0  12913  grpinvfvalg  12920  grpsubfvalg  12923  mulgfvalg  12990  mulgval  12991  mulgnn0p1  12999  issubg  13038  isnsg  13067  eqgfval  13086  iscmn  13101  mgpvalg  13138  issrg  13153  isring  13188  iscrng  13191  opprvalg  13246  isnzr  13330  islring  13338  issubrg  13347  islmod  13386  scaffvalg  13401  lsssetm  13449  lspfval  13480  istps  13617  cldval  13684  ntrfval  13685  clsfval  13686  neifval  13725  restbasg  13753  tgrest  13754  txval  13840  upxp  13857  uptx  13859  txrest  13861  lmcn2  13865  cnmpt2t  13878  cnmpt2res  13882  imasnopn  13884  psmetxrge0  13917  xmetge0  13950  isxms  14036  isms  14038  bdxmet  14086  qtopbasss  14106  cnblcld  14120  negfcncf  14174  dvfvalap  14235  eldvap  14236  dvidlemap  14245  dvexp2  14261  dvrecap  14262  dveflem  14272  sin0pilem1  14287  ptolemy  14330  coskpi  14354  logbrec  14463  lgslem1  14486  lgsval  14490  lgsval4  14506  lgsfcl3  14507  lgsdilem  14513  lgsdir2lem4  14517  lgsdir2lem5  14518  nninfsellemqall  14849