Theorem eqtr4id 2239

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 2191	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2237	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  iftrue  3551  iffalse  3554  difprsn1  3743  dmmptg  5138  relcoi1  5172  funimacnv  5304  dmmptd  5358  dffv3g  5523  dfimafn  5577  fvco2  5598  isoini  5832  oprabco  6232  ixpconstg  6721  unfiexmid  6931  undifdc  6937  sbthlemi4  6973  sbthlemi5  6974  sbthlemi6  6975  supval2ti  7008  exmidfodomrlemim  7214  suplocexprlemex  7735  eqneg  8703  zeo  9372  fseq1p1m1  10108  seq3val  10472  seqvalcd  10473  hashfzo  10816  hashxp  10820  fsumconst  11476  modfsummod  11480  telfsumo  11488  fprodconst  11642  mulgcd  12031  algcvg  12062  phiprmpw  12236  phisum  12254  strslfv3  12522  resseqnbasd  12547  imasplusg  12747  imasmulr  12748  ismgmid  12815  subrg1  13451  2idlbas  13703  uptx  14070  resubmet  14344  lgsval4lem  14708  m1lgs  14748