Theorem sylan9eqr 2289

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 2287	. 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 2216

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

This theorem is referenced by:  sbcied2  3083  csbied2  3189  fun2ssres  5401  fcoi1  5552  fcoi2  5553  funssfv  5701  caovimo  6256  mpomptsx  6406  dmmpossx  6408  fmpox  6409  2ndconst  6431  mpoxopoveq  6484  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  rdgivallem  6625  nnmass  6733  nnm00  6776  mapsnend  7065  ssenen  7118  fi0  7275  nnnninf2  7431  nnnninfeq2  7433  exmidfodomrlemim  7517  ltexnqq  7739  ltrnqg  7751  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  nq0a0  7788  addnqprllem  7858  addnqprulem  7859  map2psrprg  8136  rereceu  8220  addid0  8663  nnnn0addcl  9546  zindd  9717  qaddcl  9988  qmulcl  9990  qreccl  9995  xaddpnf1  10201  xaddmnf1  10203  xaddnemnf  10212  xaddnepnf  10213  xaddcom  10216  xnegdi  10223  xaddass  10224  xpncan  10226  xleadd1a  10228  xltadd1  10231  xlt2add  10235  modfzo0difsn  10784  frec2uzrdg  10798  seqf1oglem2  10909  expp1  10935  expnegap0  10936  expcllem  10939  mulexp  10967  expmul  10973  sqoddm1div8  11083  bcpasc  11156  hashfzo  11215  lsw0  11300  ccatval1  11313  ccatval2  11314  swrdval  11368  ccatopth  11436  reuccatpfxs1  11467  shftfn  11537  reim0b  11575  cjexp  11606  sumsnf  12124  binomlem  12198  prodsnf  12307  ef0lem  12375  dvdsnegb  12523  m1expe  12614  m1expo  12615  m1exp1  12616  flodddiv4  12651  gcdabs  12713  bezoutr1  12758  dvdslcm  12795  lcmeq0  12797  lcmcl  12798  lcmabs  12802  lcmgcdlem  12803  lcmdvds  12805  mulgcddvds  12820  qredeu  12823  divgcdcoprmex  12828  pcge0  13040  pcgcd1  13055  pcadd  13067  pcmpt2  13071  mulgfvalg  13878  mulgnn0subcl  13892  mulgnn0z  13906  f1ghm0to0  14029  srgmulgass  14236  srgpcomp  14237  ringinvnzdiv  14297  lmodvsmmulgdi  14601  znval  14914  mplvalcoe  14975  isxmet2d  15343  blfvalps  15380  blssioo  15548  efper  15802  relogbcxpbap  15960  logbgcd1irr  15962  lgsdir  16038  lgsne0  16041  lgsdirnn0  16050  lgsdinn0  16051  lgsquadlem2  16081  2lgslem3a  16096  2lgslem3b  16097  2lgslem3c  16098  2lgslem3d  16099  2lgslem3a1  16100  2lgslem3b1  16101  2lgslem3c1  16102  2lgslem3d1  16103  wlklenvm1  16466  wlklenvm1g  16467  wlk0prc  16497  clwwlkn2  16546  trirec0xor  16969