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  6516  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  rdgivallem  6657  nnmass  6765  nnm00  6808  mapsnend  7105  ssenen  7158  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  9775  qaddcl  10051  qmulcl  10053  qreccl  10058  xaddpnf1  10265  xaddmnf1  10267  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnegdi  10287  xaddass  10288  xpncan  10290  xleadd1a  10292  xltadd1  10295  xlt2add  10299  modfzo0difsn  10853  frec2uzrdg  10867  seqf1oglem2  10978  expp1  11004  expnegap0  11005  expcllem  11008  mulexp  11036  expmul  11042  sqoddm1div8  11152  bcpasc  11226  hashfzo  11285  hashf1lem1  11307  lsw0  11374  ccatval1  11387  ccatval2  11388  swrdval  11442  ccatopth  11510  reuccatpfxs1  11541  shftfn  11611  reim0b  11649  cjexp  11680  sumsnf  12201  binomlem  12275  prodsnf  12384  ef0lem  12452  dvdsnegb  12600  m1expe  12691  m1expo  12692  m1exp1  12693  flodddiv4  12728  gcdabs  12790  bezoutr1  12835  dvdslcm  12872  lcmeq0  12874  lcmcl  12875  lcmabs  12879  lcmgcdlem  12880  lcmdvds  12882  mulgcddvds  12897  qredeu  12900  divgcdcoprmex  12905  pcge0  13121  pcgcd1  13136  pcadd  13148  pcmpt2  13152  mulgfvalg  13983  mulgnn0subcl  13997  mulgnn0z  14011  f1ghm0to0  14134  gsumresfi  14263  srgmulgass  14400  srgpcomp  14401  ringinvnzdiv  14462  lmodvsmmulgdi  14769  znval  15080  assamulgscmlem2  15151  mplvalg  15234  isxmet2d  15607  blfvalps  15644  blssioo  15812  efper  16067  relogbcxpbap  16234  logbgcd1irr  16236  zprmlogbaplem2  16249  chtqub  16329  bposlem2  16345  lgsdir  16392  lgsne0  16395  lgsdirnn0  16404  lgsdinn0  16405  lgsquadlem2  16435  2lgslem3a  16450  2lgslem3b  16451  2lgslem3c  16452  2lgslem3d  16453  2lgslem3a1  16454  2lgslem3b1  16455  2lgslem3c1  16456  2lgslem3d1  16457  wlklenvm1  16820  wlklenvm1g  16821  wlk0prc  16851  clwwlkn2  16900  trirec0xor  17334