Theorem eqtr4d 1131

Description: An equality transitivity equality deduction.

Hypotheses

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

Assertion

Ref	Expression
eqtr4d	⊢ (φ → A = C)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (φ → A = B)
2		eqtr4d.2	. . 3 ⊢ (φ → C = B)
3	2	cleqcomd 1106	. 2 ⊢ (φ → B = C)
4	1, 3	eqtrd 1128	1 ⊢ (φ → A = C)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  3eqtr4d 1134  3eqtr4rd 1135  opthwiener 1914  onsucmin 2323  dmsnop 2547  dmxpid 2553  imasn 2616  f1ococnv2 2817  fveqres 2851  funfv 2862  fvco 2865  fsn2 2896  fconst2 2902  ndmoprcom 3061  ndmoprass 3062  ndmoprdistr 3063  1stval 3089  2ndval 3090  1st2val 3097  oesuc 3134  oaass 3163  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  fundmen 3333  pw2en 3348  xpmapenlem3 3393  xpmapenlem5 3395  cardval 3633  unxpdomlem 3649  cardcard 3655  cardiun 3665  cfsuc 3709  distrpq 3861  recmulpq 3864  addcompr 3917  mulcompr 3919  mulcmpblnrlem 3976  0idsr 4000  1idsr 4001  mulneg12t 4198  zaddclt 4590  zltp1let 4597  uzrdgsuc 4659  expaddt 4698  nn0opth 4724  facp1t 4873  infxpidmlem4 4936  infmap2 4953  hvsub4t 5014  his5 5050  pjpot 5265  hsupvalt 5302  spanid 5318  shjcomt 5331  h1de2b 5459  spanunsn 5482  hosdir 5609  hoddir 5610  ho1 5613  pjscj 5640  atcvat3 5774

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org