Theorem eqtr4id 2218

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  iftrue  3525  iffalse  3528  difprsn1  3712  dmmptg  5101  relcoi1  5135  funimacnv  5264  dmmptd  5318  dffv3g  5482  dfimafn  5535  fvco2  5555  isoini  5786  oprabco  6185  ixpconstg  6673  unfiexmid  6883  undifdc  6889  sbthlemi4  6925  sbthlemi5  6926  sbthlemi6  6927  supval2ti  6960  exmidfodomrlemim  7157  suplocexprlemex  7663  eqneg  8628  zeo  9296  fseq1p1m1  10029  seq3val  10393  seqvalcd  10394  hashfzo  10735  hashxp  10739  fsumconst  11395  modfsummod  11399  telfsumo  11407  fprodconst  11561  mulgcd  11949  algcvg  11980  phiprmpw  12154  phisum  12172  strslfv3  12439  ismgmid  12608  uptx  12914  resubmet  13188  lgsval4lem  13552