Theorem sylan9eq 1144

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
sylan9eq	⊢ ((φ ∧ ψ) → A = C)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. . 3 ⊢ (φ → A = B)
2	1	adantr 306	. 2 ⊢ ((φ ∧ ψ) → A = B)
3		sylan9eq.2	. . 3 ⊢ (ψ → B = C)
4	3	adantl 305	. 2 ⊢ ((φ ∧ ψ) → B = C)
5	2, 4	eqtrd 1128	1 ⊢ ((φ ∧ ψ) → A = C)

Syntax hints:   → wi 2   ∧ wa 196   = wceq 1091

This theorem is referenced by:  sylan9eqr 1145  uneq12 1613  ineq12 1640  ifeq12 1782  ifbi 1783  preq12b 1874  opeq12 1878  opthwiener 1914  coi2 2666  fun2ssres 2699  funimass1 2712  fndmu 2725  funssfv 2841  fvopabn 2873  fvopabgf 2874  fvopabnf 2875  rdgsucopab 2984  rdgsucopabn 2985  frsucopab 2992  abianfplem 2999  opreq12 3008  oprabval4g 3053  caoprmo 3084  oevn0 3123  oe0m1 3129  oa0r 3141  om1r 3145  oe1m 3147  map0 3268  sbthlem4 3352  sbthlem5 3353  mapenlem2 3385  mapdom2 3389  mapxpen 3390  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  phplem4 3406  phplem5 3407  addclprlem2 3913  mulclprlem 3915  reclem3pr 3952  mulcmpblnrlem 3976  supsrlem2 4020  addcnsr 4047  mulcnsr 4048  ax1id 4077  axnegex 4078  axcnre 4087  add20 4329  nndiv 4453  nn0addclt 4551  uzind 4603  om2uzran 4655  seqlem1 4662  abs00 4839  ruclem4 4888  infxpidmlem4 4936  infxpidmlem10 4942  hial0 5058  ocsh 5164  hosvalt 5489  hodvalt 5490  pjclem4 5653  pj3s 5659  strlem3a 5693  atcv0eq 5767  atcv1 5768

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