Theorem eqtr4id 2261

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

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

Assertion

Ref	Expression
eqtr4id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
2		eqtr4id.2	. . 3 ⊢ 𝐴 = 𝐵
3	2	eqcomi 2213	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2259	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1375

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 1473  ax-gen 1475  ax-4 1536  ax-17 1552  ax-ext 2191

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

This theorem is referenced by:  iftrue  3587  iffalse  3590  difprsn1  3786  dmmptg  5202  relcoi1  5236  funimacnv  5373  dmmptd  5430  dffv3g  5599  dfimafn  5655  fvco2  5676  isoini  5915  iotaexel  5932  fvmpopr2d  6112  oprabco  6333  ixpconstg  6824  unfiexmid  7048  undifdc  7054  sbthlemi4  7095  sbthlemi5  7096  sbthlemi6  7097  supval2ti  7130  exmidfodomrlemim  7347  suplocexprlemex  7877  eqneg  8847  zeo  9520  fseq1p1m1  10258  seq3val  10649  seqvalcd  10650  hashfzo  11011  hashxp  11015  wrdval  11041  wrdnval  11068  swrdccat3blem  11237  fsumconst  11931  modfsummod  11935  telfsumo  11943  fprodconst  12097  mulgcd  12503  algcvg  12536  phiprmpw  12710  phisum  12729  strslfv3  13044  resseqnbasd  13072  pwssnf1o  13297  imasplusg  13307  imasmulr  13308  ismgmid  13376  pws0g  13450  dfrhm2  14083  subrg1  14160  2idlbas  14444  psrbagfi  14602  psrlinv  14613  mplbascoe  14620  mplplusgg  14632  uptx  14913  resubmet  15195  ply1termlem  15381  lgsval4lem  15655  lgsquadlem2  15722  m1lgs  15729  uspgrf1oedg  15939