Theorem sylan9eqr 2232

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  sbcied2  3001  csbied2  3105  fun2ssres  5260  fcoi1  5397  fcoi2  5398  funssfv  5542  caovimo  6068  mpomptsx  6198  dmmpossx  6200  fmpox  6201  2ndconst  6223  mpoxopoveq  6241  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  rdgivallem  6382  nnmass  6488  nnm00  6531  ssenen  6851  fi0  6974  nnnninf2  7125  nnnninfeq2  7127  exmidfodomrlemim  7200  ltexnqq  7407  ltrnqg  7419  nqnq0a  7453  nqnq0m  7454  nq0m0r  7455  nq0a0  7456  addnqprllem  7526  addnqprulem  7527  map2psrprg  7804  rereceu  7888  addid0  8330  nnnn0addcl  9206  zindd  9371  qaddcl  9635  qmulcl  9637  qreccl  9642  xaddpnf1  9846  xaddmnf1  9848  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xnegdi  9868  xaddass  9869  xpncan  9871  xleadd1a  9873  xltadd1  9876  xlt2add  9880  modfzo0difsn  10395  frec2uzrdg  10409  expp1  10527  expnegap0  10528  expcllem  10531  mulexp  10559  expmul  10565  sqoddm1div8  10674  bcpasc  10746  hashfzo  10802  shftfn  10833  reim0b  10871  cjexp  10902  sumsnf  11417  binomlem  11491  prodsnf  11600  ef0lem  11668  dvdsnegb  11815  m1expe  11904  m1expo  11905  m1exp1  11906  flodddiv4  11939  gcdabs  11989  bezoutr1  12034  dvdslcm  12069  lcmeq0  12071  lcmcl  12072  lcmabs  12076  lcmgcdlem  12077  lcmdvds  12079  mulgcddvds  12094  qredeu  12097  divgcdcoprmex  12102  pcge0  12312  pcgcd1  12327  pcadd  12339  pcmpt2  12342  mulgfvalg  12985  mulgnn0subcl  12996  mulgnn0z  13010  srgmulgass  13172  srgpcomp  13173  ringinvnzdiv  13227  lmodvsmmulgdi  13413  isxmet2d  13851  blfvalps  13888  blssioo  14048  efper  14231  relogbcxpbap  14386  logbgcd1irr  14388  lgsdir  14439  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  trirec0xor  14796