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  3562  iffalse  3565  difprsn1  3757  dmmptg  5163  relcoi1  5197  funimacnv  5330  dmmptd  5384  dffv3g  5550  dfimafn  5605  fvco2  5626  isoini  5861  iotaexel  5878  oprabco  6270  ixpconstg  6761  unfiexmid  6974  undifdc  6980  sbthlemi4  7019  sbthlemi5  7020  sbthlemi6  7021  supval2ti  7054  exmidfodomrlemim  7261  suplocexprlemex  7782  eqneg  8751  zeo  9422  fseq1p1m1  10160  seq3val  10531  seqvalcd  10532  hashfzo  10893  hashxp  10897  wrdval  10917  wrdnval  10944  fsumconst  11597  modfsummod  11601  telfsumo  11609  fprodconst  11763  mulgcd  12153  algcvg  12186  phiprmpw  12360  phisum  12378  strslfv3  12664  resseqnbasd  12691  imasplusg  12891  imasmulr  12892  ismgmid  12960  dfrhm2  13650  subrg1  13727  2idlbas  14011  uptx  14442  resubmet  14716  ply1termlem  14888  lgsval4lem  15127  m1lgs  15192