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-1 5  ax-2 6  ax-3 7  ax-mp 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  2854  rabeqbidva  2855  csbidmg  3190  csbco3g  3193  difeq12d  3386  ifeq12d  3678  ifbieq2d  3682  ifbieq12d  3684  csbsng  3785  csbunig  3899  iuneq12d  3993  iinrab2  4029  riinrab  4041  cokeq12d  4237  pw1eqadj  4332  iotaint  4352  dfiota4  4372  ssfin  4470  tfinltfinlem1  4500  oddtfin  4518  opeq12d  4586  csbxpg  4813  coeq12d  4881  reseq12d  4935  imaeq12d  4943  csbrng  4966  csbresg  4976  dfxp2  5113  funprg  5149  funprgOLD  5150  imain  5172  fnco  5191  foima  5274  f1imacnv  5302  f1ococnv2  5309  fveq12d  5333  csbfv12g  5336  csbfv2g  5337  csbfvg  5338  fvun1  5379  fvresi  5443  csbov12g  5553  csbov1g  5554  csbov2g  5555  fmpt2x  5730  fvfullfun  5864  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  sbthlem3  6205  muc0or  6252  nmembers1  6271  nchoicelem1  6289  nchoicelem2  6290  nchoicelem3  6291  nchoicelem7  6295