Theorem sylan9eq 2291

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
sylan9eq.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9eq	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eq.2	. 2 ⊢ (𝜓 → 𝐵 = 𝐶)
3		eqtr 2256	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  sylan9req  2292  sylan9eqr  2293  difeq12  3342  uneq12  3378  ineq12  3427  ifeq12  3657  preq12  3790  prprc  3823  preq12b  3895  opeq12  3906  xpeq12  4793  nfimad  5135  coi2  5304  funimass1  5458  f1orescnv  5655  resdif  5661  oveq12  6094  cbvmpov  6168  ovmpog  6223  fvmpopr2d  6225  eqopi  6406  fmpoco  6452  supp0cosupp0fn  6507  imacosuppfn  6508  nnaordex  6801  map0g  6969  xpcomco  7124  xpmapenlem  7149  phplem3  7155  phplem4  7156  sbthlemi5  7278  addcmpblnq  7734  ltrnqg  7787  enq0ref  7800  addcmpblnq0  7810  distrlem4prl  7951  distrlem4pru  7952  recexgt0sr  8140  axcnre  8248  cnegexlem2  8502  cnegexlem3  8503  recexap  8981  xaddpnf2  10249  xaddmnf2  10251  rexadd  10254  xaddnemnf  10259  xaddnepnf  10260  xposdif  10284  frec2uzrand  10842  seqeq3  10889  seqf1oglem2  10957  seqf1og  10958  lsw1  11354  swrdccat  11507  ccats1pfxeqbi  11514  shftcan1  11599  remul2  11638  immul2  11645  fprodssdc  12357  ef0lem  12427  efieq1re  12539  dvdsnegb  12575  dvdscmul  12585  dvds2ln  12591  dvds2add  12592  dvds2sub  12593  gcdn0val  12738  rpmulgcd  12803  lcmval  12841  lcmn0val  12844  odzval  13020  pcmpt  13122  ballotfilemfp1  13231  grpsubval  13851  mulgnn0gzsum  13931  crngpropd  14344  opprringbg  14385  dvdsrtr  14408  isopn3  15226  dvexp  15812  dvexp2  15813  elply2  15836  lgsval3  16137  lgsdinn0  16167  incistruhgr  16331  clwwlkn1loopb  16661  clwwlkext2edg  16663  clwwlknonex2  16680  eupth2lem3lem3fi  16711  subctctexmid  17030