Theorem eqtrd 2385

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrd.1	⊢ (φ → A = B)
eqtrd.2	⊢ (φ → B = C)

Assertion

Ref	Expression
eqtrd	⊢ (φ → A = C)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (φ → A = B)
2		eqtrd.2	. . 3 ⊢ (φ → B = C)
3	2	eqeq2d 2364	. 2 ⊢ (φ → (A = B ↔ A = C))
4	1, 3	mpbid 201	1 ⊢ (φ → A = C)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  eqtr2d  2386  eqtr3d  2387  eqtr4d  2388  3eqtrd  2389  3eqtrrd  2390  3eqtr2d  2391  syl5eq  2397  syl6eq  2401  rabeqbidv  2855  rabeqbidva  2856  csbidmg  3191  csbco3g  3194  difeq12d  3387  ifeq12d  3679  ifbieq2d  3683  ifbieq12d  3685  csbsng  3786  csbunig  3900  iuneq12d  3994  iinrab2  4030  riinrab  4042  cokeq12d  4238  pw1eqadj  4333  iotaint  4353  dfiota4  4373  ssfin  4471  tfinltfinlem1  4501  oddtfin  4519  opeq12d  4587  csbxpg  4814  coeq12d  4882  reseq12d  4936  imaeq12d  4944  csbrng  4967  csbresg  4977  dfxp2  5114  funprg  5150  funprgOLD  5151  imain  5173  fnco  5192  foima  5275  f1imacnv  5303  f1ococnv2  5310  fveq12d  5334  csbfv12g  5337  csbfv2g  5338  csbfvg  5339  fvun1  5380  fvresi  5444  csbov12g  5554  csbov1g  5555  csbov2g  5556  fmpt2x  5731  fvfullfun  5865  enmap2lem5  6068  enmap1lem5  6074  enprmaplem5  6081  sbthlem3  6206  muc0or  6253  nmembers1  6272  nchoicelem1  6290  nchoicelem2  6291  nchoicelem3  6292  nchoicelem7  6296