Theorem eqtr4id 2248

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 2200	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2246	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  iftrue  3566  iffalse  3569  difprsn1  3761  dmmptg  5167  relcoi1  5201  funimacnv  5334  dmmptd  5388  dffv3g  5554  dfimafn  5609  fvco2  5630  isoini  5865  iotaexel  5882  fvmpopr2d  6059  oprabco  6275  ixpconstg  6766  unfiexmid  6979  undifdc  6985  sbthlemi4  7026  sbthlemi5  7027  sbthlemi6  7028  supval2ti  7061  exmidfodomrlemim  7268  suplocexprlemex  7789  eqneg  8759  zeo  9431  fseq1p1m1  10169  seq3val  10552  seqvalcd  10553  hashfzo  10914  hashxp  10918  wrdval  10938  wrdnval  10965  fsumconst  11619  modfsummod  11623  telfsumo  11631  fprodconst  11785  mulgcd  12183  algcvg  12216  phiprmpw  12390  phisum  12409  strslfv3  12724  resseqnbasd  12751  imasplusg  12951  imasmulr  12952  ismgmid  13020  dfrhm2  13710  subrg1  13787  2idlbas  14071  uptx  14510  resubmet  14792  ply1termlem  14978  lgsval4lem  15252  lgsquadlem2  15319  m1lgs  15326