Theorem sylan9eqr 2286

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eqr.2	. . 3 ⊢ (𝜓 → 𝐵 = 𝐶)
3	1, 2	sylan9eq 2284	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 268	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  sbcied2  3070  csbied2  3176  fun2ssres  5377  fcoi1  5525  fcoi2  5526  funssfv  5674  caovimo  6226  mpomptsx  6371  dmmpossx  6373  fmpox  6374  2ndconst  6396  mpoxopoveq  6449  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  rdgivallem  6590  nnmass  6698  nnm00  6741  ssenen  7080  fi0  7217  nnnninf2  7369  nnnninfeq2  7371  exmidfodomrlemim  7455  ltexnqq  7671  ltrnqg  7683  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  nq0a0  7720  addnqprllem  7790  addnqprulem  7791  map2psrprg  8068  rereceu  8152  addid0  8595  nnnn0addcl  9475  zindd  9641  qaddcl  9912  qmulcl  9914  qreccl  9919  xaddpnf1  10124  xaddmnf1  10126  xaddnemnf  10135  xaddnepnf  10136  xaddcom  10139  xnegdi  10146  xaddass  10147  xpncan  10149  xleadd1a  10151  xltadd1  10154  xlt2add  10158  modfzo0difsn  10701  frec2uzrdg  10715  seqf1oglem2  10826  expp1  10852  expnegap0  10853  expcllem  10856  mulexp  10884  expmul  10890  sqoddm1div8  10999  bcpasc  11072  hashfzo  11130  lsw0  11208  ccatval1  11221  ccatval2  11222  swrdval  11276  ccatopth  11344  reuccatpfxs1  11375  shftfn  11445  reim0b  11483  cjexp  11514  sumsnf  12031  binomlem  12105  prodsnf  12214  ef0lem  12282  dvdsnegb  12430  m1expe  12521  m1expo  12522  m1exp1  12523  flodddiv4  12558  gcdabs  12620  bezoutr1  12665  dvdslcm  12702  lcmeq0  12704  lcmcl  12705  lcmabs  12709  lcmgcdlem  12710  lcmdvds  12712  mulgcddvds  12727  qredeu  12730  divgcdcoprmex  12735  pcge0  12947  pcgcd1  12962  pcadd  12974  pcmpt2  12978  mulgfvalg  13769  mulgnn0subcl  13783  mulgnn0z  13797  f1ghm0to0  13920  srgmulgass  14064  srgpcomp  14065  ringinvnzdiv  14125  lmodvsmmulgdi  14399  znval  14712  mplvalcoe  14771  isxmet2d  15139  blfvalps  15176  blssioo  15344  efper  15598  relogbcxpbap  15756  logbgcd1irr  15758  lgsdir  15834  lgsne0  15837  lgsdirnn0  15846  lgsdinn0  15847  lgsquadlem2  15877  2lgslem3a  15892  2lgslem3b  15893  2lgslem3c  15894  2lgslem3d  15895  2lgslem3a1  15896  2lgslem3b1  15897  2lgslem3c1  15898  2lgslem3d1  15899  wlklenvm1  16262  wlklenvm1g  16263  wlk0prc  16293  clwwlkn2  16342  trirec0xor  16757