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  5421  fcoi1  5572  fcoi2  5573  funssfv  5721  caovimo  6283  mpomptsx  6433  dmmpossx  6435  fmpox  6436  2ndconst  6458  mpoxopoveq  6511  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  rdgivallem  6652  nnmass  6760  nnm00  6803  mapsnend  7099  ssenen  7152  fi0  7309  nnnninf2  7468  nnnninfeq2  7470  exmidfodomrlemim  7554  ltexnqq  7776  ltrnqg  7788  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  nq0a0  7825  addnqprllem  7895  addnqprulem  7896  map2psrprg  8173  rereceu  8257  addid0  8701  nnnn0addcl  9598  zindd  9769  qaddcl  10045  qmulcl  10047  qreccl  10052  xaddpnf1  10259  xaddmnf1  10261  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnegdi  10281  xaddass  10282  xpncan  10284  xleadd1a  10286  xltadd1  10289  xlt2add  10293  modfzo0difsn  10846  frec2uzrdg  10860  seqf1oglem2  10971  expp1  10997  expnegap0  10998  expcllem  11001  mulexp  11029  expmul  11035  sqoddm1div8  11145  bcpasc  11219  hashfzo  11278  hashf1lem1  11300  lsw0  11367  ccatval1  11380  ccatval2  11381  swrdval  11435  ccatopth  11503  reuccatpfxs1  11534  shftfn  11604  reim0b  11642  cjexp  11673  sumsnf  12194  binomlem  12268  prodsnf  12377  ef0lem  12445  dvdsnegb  12593  m1expe  12684  m1expo  12685  m1exp1  12686  flodddiv4  12721  gcdabs  12783  bezoutr1  12828  dvdslcm  12865  lcmeq0  12867  lcmcl  12868  lcmabs  12872  lcmgcdlem  12873  lcmdvds  12875  mulgcddvds  12890  qredeu  12893  divgcdcoprmex  12898  pcge0  13114  pcgcd1  13129  pcadd  13141  pcmpt2  13145  mulgfvalg  13975  mulgnn0subcl  13989  mulgnn0z  14003  f1ghm0to0  14126  srgmulgass  14344  srgpcomp  14345  ringinvnzdiv  14406  lmodvsmmulgdi  14711  znval  15022  assamulgscmlem2  15093  mplvalcoe  15133  isxmet2d  15501  blfvalps  15538  blssioo  15706  efper  15961  relogbcxpbap  16123  logbgcd1irr  16125  zprmlogbaplem2  16138  chtqub  16218  bposlem2  16234  lgsdir  16276  lgsne0  16279  lgsdirnn0  16288  lgsdinn0  16289  lgsquadlem2  16319  2lgslem3a  16334  2lgslem3b  16335  2lgslem3c  16336  2lgslem3d  16337  2lgslem3a1  16338  2lgslem3b1  16339  2lgslem3c1  16340  2lgslem3d1  16341  wlklenvm1  16704  wlklenvm1g  16705  wlk0prc  16735  clwwlkn2  16784  trirec0xor  17216