Theorem sylan9eqr 2251

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 2249	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 268	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  sbcied2  3027  csbied2  3132  fun2ssres  5302  fcoi1  5441  fcoi2  5442  funssfv  5587  caovimo  6121  mpomptsx  6264  dmmpossx  6266  fmpox  6267  2ndconst  6289  mpoxopoveq  6307  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  rdgivallem  6448  nnmass  6554  nnm00  6597  ssenen  6921  fi0  7050  nnnninf2  7202  nnnninfeq2  7204  exmidfodomrlemim  7282  ltexnqq  7494  ltrnqg  7506  nqnq0a  7540  nqnq0m  7541  nq0m0r  7542  nq0a0  7543  addnqprllem  7613  addnqprulem  7614  map2psrprg  7891  rereceu  7975  addid0  8418  nnnn0addcl  9298  zindd  9463  qaddcl  9728  qmulcl  9730  qreccl  9735  xaddpnf1  9940  xaddmnf1  9942  xaddnemnf  9951  xaddnepnf  9952  xaddcom  9955  xnegdi  9962  xaddass  9963  xpncan  9965  xleadd1a  9967  xltadd1  9970  xlt2add  9974  modfzo0difsn  10506  frec2uzrdg  10520  seqf1oglem2  10631  expp1  10657  expnegap0  10658  expcllem  10661  mulexp  10689  expmul  10695  sqoddm1div8  10804  bcpasc  10877  hashfzo  10933  shftfn  11008  reim0b  11046  cjexp  11077  sumsnf  11593  binomlem  11667  prodsnf  11776  ef0lem  11844  dvdsnegb  11992  m1expe  12083  m1expo  12084  m1exp1  12085  flodddiv4  12120  gcdabs  12182  bezoutr1  12227  dvdslcm  12264  lcmeq0  12266  lcmcl  12267  lcmabs  12271  lcmgcdlem  12272  lcmdvds  12274  mulgcddvds  12289  qredeu  12292  divgcdcoprmex  12297  pcge0  12509  pcgcd1  12524  pcadd  12536  pcmpt2  12540  mulgfvalg  13329  mulgnn0subcl  13343  mulgnn0z  13357  f1ghm0to0  13480  srgmulgass  13623  srgpcomp  13624  ringinvnzdiv  13684  lmodvsmmulgdi  13957  znval  14270  mplvalcoe  14324  isxmet2d  14692  blfvalps  14729  blssioo  14897  efper  15151  relogbcxpbap  15309  logbgcd1irr  15311  lgsdir  15384  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  lgsquadlem2  15427  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  trirec0xor  15802