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  3066  csbied2  3172  fun2ssres  5357  fcoi1  5502  fcoi2  5503  funssfv  5649  caovimo  6190  mpomptsx  6333  dmmpossx  6335  fmpox  6336  2ndconst  6358  mpoxopoveq  6376  tfrlemisucaccv  6461  tfr1onlemsucaccv  6477  tfrcllemsucaccv  6490  rdgivallem  6517  nnmass  6623  nnm00  6666  ssenen  7000  fi0  7130  nnnninf2  7282  nnnninfeq2  7284  exmidfodomrlemim  7367  ltexnqq  7583  ltrnqg  7595  nqnq0a  7629  nqnq0m  7630  nq0m0r  7631  nq0a0  7632  addnqprllem  7702  addnqprulem  7703  map2psrprg  7980  rereceu  8064  addid0  8507  nnnn0addcl  9387  zindd  9553  qaddcl  9818  qmulcl  9820  qreccl  9825  xaddpnf1  10030  xaddmnf1  10032  xaddnemnf  10041  xaddnepnf  10042  xaddcom  10045  xnegdi  10052  xaddass  10053  xpncan  10055  xleadd1a  10057  xltadd1  10060  xlt2add  10064  modfzo0difsn  10604  frec2uzrdg  10618  seqf1oglem2  10729  expp1  10755  expnegap0  10756  expcllem  10759  mulexp  10787  expmul  10793  sqoddm1div8  10902  bcpasc  10975  hashfzo  11031  lsw0  11105  ccatval1  11118  ccatval2  11119  swrdval  11166  ccatopth  11234  reuccatpfxs1  11265  shftfn  11321  reim0b  11359  cjexp  11390  sumsnf  11906  binomlem  11980  prodsnf  12089  ef0lem  12157  dvdsnegb  12305  m1expe  12396  m1expo  12397  m1exp1  12398  flodddiv4  12433  gcdabs  12495  bezoutr1  12540  dvdslcm  12577  lcmeq0  12579  lcmcl  12580  lcmabs  12584  lcmgcdlem  12585  lcmdvds  12587  mulgcddvds  12602  qredeu  12605  divgcdcoprmex  12610  pcge0  12822  pcgcd1  12837  pcadd  12849  pcmpt2  12853  mulgfvalg  13644  mulgnn0subcl  13658  mulgnn0z  13672  f1ghm0to0  13795  srgmulgass  13938  srgpcomp  13939  ringinvnzdiv  13999  lmodvsmmulgdi  14272  znval  14585  mplvalcoe  14639  isxmet2d  15007  blfvalps  15044  blssioo  15212  efper  15466  relogbcxpbap  15624  logbgcd1irr  15626  lgsdir  15699  lgsne0  15702  lgsdirnn0  15711  lgsdinn0  15712  lgsquadlem2  15742  2lgslem3a  15757  2lgslem3b  15758  2lgslem3c  15759  2lgslem3d  15760  2lgslem3a1  15761  2lgslem3b1  15762  2lgslem3c1  15763  2lgslem3d1  15764  trirec0xor  16344