Theorem eqtr4id 2245

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  iftrue  3563  iffalse  3566  difprsn1  3758  dmmptg  5164  relcoi1  5198  funimacnv  5331  dmmptd  5385  dffv3g  5551  dfimafn  5606  fvco2  5627  isoini  5862  iotaexel  5879  fvmpopr2d  6056  oprabco  6272  ixpconstg  6763  unfiexmid  6976  undifdc  6982  sbthlemi4  7021  sbthlemi5  7022  sbthlemi6  7023  supval2ti  7056  exmidfodomrlemim  7263  suplocexprlemex  7784  eqneg  8753  zeo  9425  fseq1p1m1  10163  seq3val  10534  seqvalcd  10535  hashfzo  10896  hashxp  10900  wrdval  10920  wrdnval  10947  fsumconst  11600  modfsummod  11604  telfsumo  11612  fprodconst  11766  mulgcd  12156  algcvg  12189  phiprmpw  12363  phisum  12381  strslfv3  12667  resseqnbasd  12694  imasplusg  12894  imasmulr  12895  ismgmid  12963  dfrhm2  13653  subrg1  13730  2idlbas  14014  uptx  14453  resubmet  14735  ply1termlem  14921  lgsval4lem  15168  lgsquadlem2  15235  m1lgs  15242