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  7467  nnnninfeq2  7469  exmidfodomrlemim  7553  ltexnqq  7775  ltrnqg  7787  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  addnqprllem  7894  addnqprulem  7895  map2psrprg  8172  rereceu  8256  addid0  8699  nnnn0addcl  9595  zindd  9766  qaddcl  10037  qmulcl  10039  qreccl  10044  xaddpnf1  10250  xaddmnf1  10252  xaddnemnf  10261  xaddnepnf  10262  xaddcom  10265  xnegdi  10272  xaddass  10273  xpncan  10275  xleadd1a  10277  xltadd1  10280  xlt2add  10284  modfzo0difsn  10834  frec2uzrdg  10848  seqf1oglem2  10959  expp1  10985  expnegap0  10986  expcllem  10989  mulexp  11017  expmul  11023  sqoddm1div8  11133  bcpasc  11206  hashfzo  11265  hashf1lem1  11287  lsw0  11354  ccatval1  11367  ccatval2  11368  swrdval  11422  ccatopth  11490  reuccatpfxs1  11521  shftfn  11591  reim0b  11629  cjexp  11660  sumsnf  12178  binomlem  12252  prodsnf  12361  ef0lem  12429  dvdsnegb  12577  m1expe  12668  m1expo  12669  m1exp1  12670  flodddiv4  12705  gcdabs  12767  bezoutr1  12812  dvdslcm  12849  lcmeq0  12851  lcmcl  12852  lcmabs  12856  lcmgcdlem  12857  lcmdvds  12859  mulgcddvds  12874  qredeu  12877  divgcdcoprmex  12882  pcge0  13094  pcgcd1  13109  pcadd  13121  pcmpt2  13125  mulgfvalg  13926  mulgnn0subcl  13940  mulgnn0z  13954  f1ghm0to0  14077  srgmulgass  14295  srgpcomp  14296  ringinvnzdiv  14357  lmodvsmmulgdi  14662  znval  14973  assamulgscmlem2  15044  mplvalcoe  15083  isxmet2d  15451  blfvalps  15488  blssioo  15656  efper  15911  relogbcxpbap  16073  logbgcd1irr  16075  lgsdir  16166  lgsne0  16169  lgsdirnn0  16178  lgsdinn0  16179  lgsquadlem2  16209  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  wlklenvm1  16594  wlklenvm1g  16595  wlk0prc  16625  clwwlkn2  16674  trirec0xor  17106