Theorem sylan9eqr 2284

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  sbcied2  3067  csbied2  3173  fun2ssres  5367  fcoi1  5514  fcoi2  5515  funssfv  5661  caovimo  6211  mpomptsx  6357  dmmpossx  6359  fmpox  6360  2ndconst  6382  mpoxopoveq  6401  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  rdgivallem  6542  nnmass  6650  nnm00  6693  ssenen  7032  fi0  7168  nnnninf2  7320  nnnninfeq2  7322  exmidfodomrlemim  7405  ltexnqq  7621  ltrnqg  7633  nqnq0a  7667  nqnq0m  7668  nq0m0r  7669  nq0a0  7670  addnqprllem  7740  addnqprulem  7741  map2psrprg  8018  rereceu  8102  addid0  8545  nnnn0addcl  9425  zindd  9591  qaddcl  9862  qmulcl  9864  qreccl  9869  xaddpnf1  10074  xaddmnf1  10076  xaddnemnf  10085  xaddnepnf  10086  xaddcom  10089  xnegdi  10096  xaddass  10097  xpncan  10099  xleadd1a  10101  xltadd1  10104  xlt2add  10108  modfzo0difsn  10650  frec2uzrdg  10664  seqf1oglem2  10775  expp1  10801  expnegap0  10802  expcllem  10805  mulexp  10833  expmul  10839  sqoddm1div8  10948  bcpasc  11021  hashfzo  11079  lsw0  11154  ccatval1  11167  ccatval2  11168  swrdval  11222  ccatopth  11290  reuccatpfxs1  11321  shftfn  11378  reim0b  11416  cjexp  11447  sumsnf  11963  binomlem  12037  prodsnf  12146  ef0lem  12214  dvdsnegb  12362  m1expe  12453  m1expo  12454  m1exp1  12455  flodddiv4  12490  gcdabs  12552  bezoutr1  12597  dvdslcm  12634  lcmeq0  12636  lcmcl  12637  lcmabs  12641  lcmgcdlem  12642  lcmdvds  12644  mulgcddvds  12659  qredeu  12662  divgcdcoprmex  12667  pcge0  12879  pcgcd1  12894  pcadd  12906  pcmpt2  12910  mulgfvalg  13701  mulgnn0subcl  13715  mulgnn0z  13729  f1ghm0to0  13852  srgmulgass  13995  srgpcomp  13996  ringinvnzdiv  14056  lmodvsmmulgdi  14330  znval  14643  mplvalcoe  14697  isxmet2d  15065  blfvalps  15102  blssioo  15270  efper  15524  relogbcxpbap  15682  logbgcd1irr  15684  lgsdir  15757  lgsne0  15760  lgsdirnn0  15769  lgsdinn0  15770  lgsquadlem2  15800  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  wlklenvm1  16152  wlklenvm1g  16153  wlk0prc  16183  clwwlkn2  16230  trirec0xor  16599