Theorem eqtr4id 2283

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 2235	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2281	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:  iftrue  3610  iffalse  3613  difprsn1  3812  dmmptg  5234  relcoi1  5268  funimacnv  5406  dmmptd  5463  dffv3g  5635  dfimafn  5694  fvco2  5715  isoini  5959  iotaexel  5976  fvmpopr2d  6158  oprabco  6382  ixpconstg  6876  unfiexmid  7110  undifdc  7116  sbthlemi4  7159  sbthlemi5  7160  sbthlemi6  7161  supval2ti  7194  exmidfodomrlemim  7412  suplocexprlemex  7942  eqneg  8912  zeo  9585  fseq1p1m1  10329  seq3val  10723  seqvalcd  10724  hashfzo  11087  hashxp  11091  wrdval  11117  wrdnval  11145  swrdccat3blem  11321  fsumconst  12017  modfsummod  12021  telfsumo  12029  fprodconst  12183  mulgcd  12589  algcvg  12622  phiprmpw  12796  phisum  12815  strslfv3  13130  resseqnbasd  13158  pwssnf1o  13383  imasplusg  13393  imasmulr  13394  ismgmid  13462  pws0g  13536  dfrhm2  14171  subrg1  14248  2idlbas  14532  psrbagfi  14690  psrlinv  14701  mplbascoe  14708  mplplusgg  14720  uptx  15001  resubmet  15283  ply1termlem  15469  lgsval4lem  15743  lgsquadlem2  15810  m1lgs  15817  uspgrf1oedg  16030  gsumgfsumlem  16704