Theorem sylan9eqr 2293

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  sbcied2  3089  csbied2  3195  fun2ssres  5424  fcoi1  5575  fcoi2  5576  funssfv  5724  caovimo  6286  mpomptsx  6437  dmmpossx  6439  fmpox  6440  2ndconst  6462  mpoxopoveq  6515  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  rdgivallem  6656  nnmass  6764  nnm00  6807  mapsnend  7104  ssenen  7157  fi0  7315  nnnninf2  7474  nnnninfeq2  7476  exmidfodomrlemim  7560  ltexnqq  7782  ltrnqg  7794  nqnq0a  7828  nqnq0m  7829  nq0m0r  7830  nq0a0  7831  addnqprllem  7901  addnqprulem  7902  map2psrprg  8179  rereceu  8263  addid0  8707  nnnn0addcl  9605  zindd  9776  qaddcl  10052  qmulcl  10054  qreccl  10059  xaddpnf1  10266  xaddmnf1  10268  xaddnemnf  10277  xaddnepnf  10278  xaddcom  10281  xnegdi  10288  xaddass  10289  xpncan  10291  xleadd1a  10293  xltadd1  10296  xlt2add  10300  modfzo0difsn  10854  frec2uzrdg  10868  seqf1oglem2  10979  expp1  11005  expnegap0  11006  expcllem  11009  mulexp  11037  expmul  11043  sqoddm1div8  11153  bcpasc  11227  hashfzo  11286  hashf1lem1  11308  lsw0  11375  ccatval1  11388  ccatval2  11389  swrdval  11443  ccatopth  11511  reuccatpfxs1  11542  shftfn  11612  reim0b  11650  cjexp  11681  sumsnf  12202  binomlem  12276  prodsnf  12385  ef0lem  12453  dvdsnegb  12601  m1expe  12692  m1expo  12693  m1exp1  12694  flodddiv4  12729  gcdabs  12791  bezoutr1  12836  dvdslcm  12873  lcmeq0  12875  lcmcl  12876  lcmabs  12880  lcmgcdlem  12881  lcmdvds  12883  mulgcddvds  12898  qredeu  12901  divgcdcoprmex  12906  pcge0  13122  pcgcd1  13137  pcadd  13149  pcmpt2  13153  mulgfvalg  13984  mulgnn0subcl  13998  mulgnn0z  14012  f1ghm0to0  14135  gsumresfi  14264  srgmulgass  14401  srgpcomp  14402  ringinvnzdiv  14463  lmodvsmmulgdi  14770  znval  15081  assamulgscmlem2  15152  mplvalcoe  15218  isxmet2d  15586  blfvalps  15623  blssioo  15791  efper  16046  relogbcxpbap  16213  logbgcd1irr  16215  zprmlogbaplem2  16228  chtqub  16308  bposlem2  16324  lgsdir  16371  lgsne0  16374  lgsdirnn0  16383  lgsdinn0  16384  lgsquadlem2  16414  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  wlklenvm1  16799  wlklenvm1g  16800  wlk0prc  16830  clwwlkn2  16879  trirec0xor  17313