Theorem eqtr4di 2282

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr4g  2289  rabxmdc  3526  ifpprsnssdc  3779  relop  4880  csbcnvg  4914  dfiun3g  4989  dfiin3g  4990  resima2  5047  relcnvfld  5270  uniabio  5297  fntpg  5386  dffn5im  5691  dfimafn2  5695  fncnvima2  5768  fmptcof  5814  fcoconst  5818  fnasrng  5827  funopsn  5829  fncofn  5831  ffnov  6124  fnovim  6129  fnrnov  6167  foov  6168  funimassov  6171  ovelimab  6172  ofc12  6258  caofinvl  6260  dftpos3  6427  tfr0dm  6487  rdgisucinc  6550  oasuc  6631  ecinxp  6778  phplem1  7037  exmidpw  7099  exmidpweq  7100  unfiin  7117  fidcenumlemr  7153  0ct  7305  ctmlemr  7306  exmidaclem  7422  pw1m  7441  indpi  7561  nqnq0pi  7657  nq0m0r  7675  addnqpr1  7781  recexgt0sr  7992  suplocsrlempr  8026  recidpipr  8075  recidpirq  8077  axrnegex  8098  nntopi  8113  cnref1o  9884  fztp  10312  fseq1m1p1  10329  fz0to4untppr  10358  frecuzrdgrrn  10669  frecuzrdgsuc  10675  frecuzrdgsuctlem  10684  seq3val  10721  seqvalcd  10722  fser0const  10796  mulexpzap  10840  expaddzap  10844  bcp1m1  11026  hash2en  11106  iswrdiz  11119  pfxccatin12lem2c  11310  cjexp  11453  rexuz3  11550  bdtri  11800  climconst  11850  sumfct  11934  zsumdc  11944  fsum3  11947  sum0  11948  fsumcnv  11997  mertenslem2  12096  zproddc  12139  fprodseq  12143  prod0  12145  prod1dc  12146  prodfct  12147  fprodcnv  12185  ef0lem  12220  efzval  12243  efival  12292  sinbnd  12312  cosbnd  12313  eucalgval  12625  eucalginv  12627  eucalglt  12628  eucalgcvga  12629  eucalg  12630  sqpweven  12746  2sqpwodd  12747  dfphi2  12791  phimullem  12796  prmdiv  12806  odzval  12813  pcval  12868  pczpre  12869  pcrec  12880  4sqlem17  12979  ennnfonelemhdmp1  13029  ennnfonelemkh  13032  ressinbasd  13156  restid2  13330  topnvalg  13333  prdsval  13355  prdsbas3  13369  pwsval  13373  pwsbas  13374  pwselbasb  13375  pwsplusgval  13377  pwsmulrval  13378  imasival  13388  imasplusg  13390  qusval  13405  xpsval  13434  ismgm  13439  plusffvalg  13444  grpidvalg  13455  igsumvalx  13471  issgrp  13485  ismnddef  13500  pws0g  13533  ismhm  13543  isgrp  13588  grpn0  13617  grpinvfvalg  13624  grpsubfvalg  13627  pwsinvg  13694  mulgfvalg  13707  mulgval  13708  mulgnn0p1  13719  issubg  13759  isnsg  13788  eqgfval  13808  quseccl0g  13817  isghm  13829  conjsubg  13863  conjsubgen  13864  iscmn  13879  mgpvalg  13935  isrng  13946  issrg  13977  isring  14012  iscrng  14015  opprvalg  14081  dfrhm2  14167  isnzr  14194  islring  14205  issubrg  14234  rrgval  14275  isdomn  14282  islmod  14304  scaffvalg  14319  lsssetm  14369  lspfval  14401  2idlval  14515  2idlvalg  14516  mulgrhm2  14623  zlmval  14640  znval  14649  znzrhfo  14661  znle2  14665  psrval  14679  mplvalcoe  14703  istps  14755  cldval  14822  ntrfval  14823  clsfval  14824  neifval  14863  restbasg  14891  tgrest  14892  txval  14978  upxp  14995  uptx  14997  txrest  14999  lmcn2  15003  cnmpt2t  15016  cnmpt2res  15020  imasnopn  15022  psmetxrge0  15055  xmetge0  15088  isxms  15174  isms  15176  bdxmet  15224  qtopbasss  15244  cnblcld  15258  mpomulcn  15289  negfcncf  15329  dvfvalap  15404  eldvap  15405  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvexp2  15435  dvrecap  15436  dveflem  15449  plyconst  15468  plycolemc  15481  sin0pilem1  15504  ptolemy  15547  coskpi  15571  logbrec  15683  mpodvdsmulf1o  15713  fsumdvdsmul  15714  lgslem1  15728  lgsval  15732  lgsval4  15748  lgsfcl3  15749  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2lem5  15760  gausslemma2dlem5  15794  lgsquadlem2  15806  iedgedgg  15911  isuhgrm  15921  isushgrm  15922  isupgren  15945  isumgren  15955  isuspgren  16007  isusgren  16008  usgrstrrepeen  16081  vtxdgfval  16138  wksfval  16172  ifpsnprss  16193  clwwlkg  16243  clwwlkn1  16268  eupthsg  16295  nninfsellemqall  16617