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  7735  ltrnqg  7788  enq0ref  7801  addcmpblnq0  7811  distrlem4prl  7952  distrlem4pru  7953  recexgt0sr  8141  axcnre  8249  cnegexlem2  8504  cnegexlem3  8505  recexap  8984  xaddpnf2  10260  xaddmnf2  10262  rexadd  10265  xaddnemnf  10270  xaddnepnf  10271  xposdif  10295  frec2uzrand  10857  seqeq3  10904  seqf1oglem2  10972  seqf1og  10973  lsw1  11370  swrdccat  11523  ccats1pfxeqbi  11530  shftcan1  11615  remul2  11654  immul2  11661  fprodssdc  12376  ef0lem  12446  efieq1re  12558  dvdsnegb  12594  dvdscmul  12604  dvds2ln  12610  dvds2add  12611  dvds2sub  12612  gcdn0val  12757  rpmulgcd  12822  lcmval  12860  lcmn0val  12863  odzval  13043  pcmpt  13145  ballotfilemfp1  13283  grpsubval  13904  mulgnn0gzsum  13984  crngpropd  14428  opprringbg  14469  dvdsrtr  14492  isopn3  15317  dvexp  15903  dvexp2  15904  elply2  15927  bposlem5  16276  lgsval3  16303  lgsdinn0  16333  incistruhgr  16497  clwwlkn1loopb  16827  clwwlkext2edg  16829  clwwlknonex2  16846  eupth2lem3lem3fi  16877  subctctexmid  17196