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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  sbcied2  3069  csbied2  3175  fun2ssres  5370  fcoi1  5517  fcoi2  5518  funssfv  5665  caovimo  6216  mpomptsx  6362  dmmpossx  6364  fmpox  6365  2ndconst  6387  mpoxopoveq  6406  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  rdgivallem  6547  nnmass  6655  nnm00  6698  ssenen  7037  fi0  7174  nnnninf2  7326  nnnninfeq2  7328  exmidfodomrlemim  7412  ltexnqq  7628  ltrnqg  7640  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  addnqprllem  7747  addnqprulem  7748  map2psrprg  8025  rereceu  8109  addid0  8552  nnnn0addcl  9432  zindd  9598  qaddcl  9869  qmulcl  9871  qreccl  9876  xaddpnf1  10081  xaddmnf1  10083  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnegdi  10103  xaddass  10104  xpncan  10106  xleadd1a  10108  xltadd1  10111  xlt2add  10115  modfzo0difsn  10658  frec2uzrdg  10672  seqf1oglem2  10783  expp1  10809  expnegap0  10810  expcllem  10813  mulexp  10841  expmul  10847  sqoddm1div8  10956  bcpasc  11029  hashfzo  11087  lsw0  11165  ccatval1  11178  ccatval2  11179  swrdval  11233  ccatopth  11301  reuccatpfxs1  11332  shftfn  11389  reim0b  11427  cjexp  11458  sumsnf  11975  binomlem  12049  prodsnf  12158  ef0lem  12226  dvdsnegb  12374  m1expe  12465  m1expo  12466  m1exp1  12467  flodddiv4  12502  gcdabs  12564  bezoutr1  12609  dvdslcm  12646  lcmeq0  12648  lcmcl  12649  lcmabs  12653  lcmgcdlem  12654  lcmdvds  12656  mulgcddvds  12671  qredeu  12674  divgcdcoprmex  12679  pcge0  12891  pcgcd1  12906  pcadd  12918  pcmpt2  12922  mulgfvalg  13713  mulgnn0subcl  13727  mulgnn0z  13741  f1ghm0to0  13864  srgmulgass  14008  srgpcomp  14009  ringinvnzdiv  14069  lmodvsmmulgdi  14343  znval  14656  mplvalcoe  14710  isxmet2d  15078  blfvalps  15115  blssioo  15283  efper  15537  relogbcxpbap  15695  logbgcd1irr  15697  lgsdir  15770  lgsne0  15773  lgsdirnn0  15782  lgsdinn0  15783  lgsquadlem2  15813  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  wlklenvm1  16198  wlklenvm1g  16199  wlk0prc  16229  clwwlkn2  16278  trirec0xor  16675