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  7280  ltexnqq  7492  ltrnqg  7504  nqnq0a  7538  nqnq0m  7539  nq0m0r  7540  nq0a0  7541  addnqprllem  7611  addnqprulem  7612  map2psrprg  7889  rereceu  7973  addid0  8416  nnnn0addcl  9296  zindd  9461  qaddcl  9726  qmulcl  9728  qreccl  9733  xaddpnf1  9938  xaddmnf1  9940  xaddnemnf  9949  xaddnepnf  9950  xaddcom  9953  xnegdi  9960  xaddass  9961  xpncan  9963  xleadd1a  9965  xltadd1  9968  xlt2add  9972  modfzo0difsn  10504  frec2uzrdg  10518  seqf1oglem2  10629  expp1  10655  expnegap0  10656  expcllem  10659  mulexp  10687  expmul  10693  sqoddm1div8  10802  bcpasc  10875  hashfzo  10931  shftfn  11006  reim0b  11044  cjexp  11075  sumsnf  11591  binomlem  11665  prodsnf  11774  ef0lem  11842  dvdsnegb  11990  m1expe  12081  m1expo  12082  m1exp1  12083  flodddiv4  12118  gcdabs  12180  bezoutr1  12225  dvdslcm  12262  lcmeq0  12264  lcmcl  12265  lcmabs  12269  lcmgcdlem  12270  lcmdvds  12272  mulgcddvds  12287  qredeu  12290  divgcdcoprmex  12295  pcge0  12507  pcgcd1  12522  pcadd  12534  pcmpt2  12538  mulgfvalg  13327  mulgnn0subcl  13341  mulgnn0z  13355  f1ghm0to0  13478  srgmulgass  13621  srgpcomp  13622  ringinvnzdiv  13682  lmodvsmmulgdi  13955  znval  14268  isxmet2d  14668  blfvalps  14705  blssioo  14873  efper  15127  relogbcxpbap  15285  logbgcd1irr  15287  lgsdir  15360  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  lgsquadlem2  15403  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  trirec0xor  15776