Theorem eqtr4id 2286

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  iftrue  3629  iffalse  3632  difprsn1  3835  dmmptg  5262  relcoi1  5296  funimacnv  5434  dmmptd  5491  dffv3g  5668  dfimafn  5727  fvco2  5748  isoini  5993  iotaexel  6010  fvmpopr2d  6192  oprabco  6415  suppcofn  6468  ixpconstg  6944  unfiexmid  7180  undifdc  7186  sbthlemi4  7232  sbthlemi5  7233  sbthlemi6  7234  supval2ti  7288  exmidfodomrlemim  7506  suplocexprlemex  8042  eqneg  9011  zeo  9689  fseq1p1m1  10435  seq3val  10829  seqvalcd  10830  hashfzo  11195  hashxp  11199  hashfibclem  11214  wrdval  11235  wrdnval  11263  swrdccat3blem  11439  fsumconst  12148  modfsummod  12152  telfsumo  12160  fprodconst  12314  mulgcd  12720  algcvg  12753  phiprmpw  12927  phisum  12946  strslfv3  13279  resseqnbasd  13307  pwssnf1o  13532  imasplusg  13542  imasmulr  13543  ismgmid  13611  pws0g  13685  dfrhm2  14321  subrg1  14399  2idlbas  14712  psrbagfi  14872  psrlinv  14888  mplbascoe  14895  mplplusgg  14907  uptx  15188  resubmet  15470  ply1termlem  15656  lgsval4lem  15933  lgsquadlem2  16000  m1lgs  16007  uspgrf1oedg  16220  gsumgfsumlem  16914