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  8662  nnnn0addcl  9543  zindd  9714  qaddcl  9985  qmulcl  9987  qreccl  9992  xaddpnf1  10198  xaddmnf1  10200  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnegdi  10220  xaddass  10221  xpncan  10223  xleadd1a  10225  xltadd1  10228  xlt2add  10232  modfzo0difsn  10781  frec2uzrdg  10795  seqf1oglem2  10906  expp1  10932  expnegap0  10933  expcllem  10936  mulexp  10964  expmul  10970  sqoddm1div8  11080  bcpasc  11153  hashfzo  11212  lsw0  11297  ccatval1  11310  ccatval2  11311  swrdval  11365  ccatopth  11433  reuccatpfxs1  11464  shftfn  11534  reim0b  11572  cjexp  11603  sumsnf  12120  binomlem  12194  prodsnf  12303  ef0lem  12371  dvdsnegb  12519  m1expe  12610  m1expo  12611  m1exp1  12612  flodddiv4  12647  gcdabs  12709  bezoutr1  12754  dvdslcm  12791  lcmeq0  12793  lcmcl  12794  lcmabs  12798  lcmgcdlem  12799  lcmdvds  12801  mulgcddvds  12816  qredeu  12819  divgcdcoprmex  12824  pcge0  13036  pcgcd1  13051  pcadd  13063  pcmpt2  13067  mulgfvalg  13922  mulgnn0subcl  13936  mulgnn0z  13950  f1ghm0to0  14073  srgmulgass  14217  srgpcomp  14218  ringinvnzdiv  14278  lmodvsmmulgdi  14583  znval  14896  mplvalcoe  14957  isxmet2d  15325  blfvalps  15362  blssioo  15530  efper  15784  relogbcxpbap  15942  logbgcd1irr  15944  lgsdir  16020  lgsne0  16023  lgsdirnn0  16032  lgsdinn0  16033  lgsquadlem2  16063  2lgslem3a  16078  2lgslem3b  16079  2lgslem3c  16080  2lgslem3d  16081  2lgslem3a1  16082  2lgslem3b1  16083  2lgslem3c1  16084  2lgslem3d1  16085  wlklenvm1  16448  wlklenvm1g  16449  wlk0prc  16479  clwwlkn2  16528  trirec0xor  16941