Theorem eqtr4id 2241

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	|- A = B
eqtr4id.1	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4id	|- ( ph -> A = C )

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 |- ( ph -> C = B )
2		eqtr4id.2	. . 3 |- A = B
3	2	eqcomi 2193	. 2 |- B = A
4	1, 3	eqtr2di 2239	1 |- ( ph -> A = C )

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 2171

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

This theorem is referenced by:  iftrue  3554  iffalse  3557  difprsn1  3746  dmmptg  5144  relcoi1  5178  funimacnv  5311  dmmptd  5365  dffv3g  5530  dfimafn  5585  fvco2  5606  isoini  5840  iotaexel  5857  oprabco  6243  ixpconstg  6734  unfiexmid  6947  undifdc  6953  sbthlemi4  6990  sbthlemi5  6991  sbthlemi6  6992  supval2ti  7025  exmidfodomrlemim  7231  suplocexprlemex  7752  eqneg  8720  zeo  9389  fseq1p1m1  10126  seq3val  10491  seqvalcd  10492  hashfzo  10837  hashxp  10841  fsumconst  11497  modfsummod  11501  telfsumo  11509  fprodconst  11663  mulgcd  12052  algcvg  12083  phiprmpw  12257  phisum  12275  strslfv3  12561  resseqnbasd  12588  imasplusg  12788  imasmulr  12789  ismgmid  12856  dfrhm2  13521  subrg1  13595  2idlbas  13847  uptx  14251  resubmet  14525  lgsval4lem  14890  m1lgs  14930