Theorem sylan9eqr 2220

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  sbcied2  2987  csbied2  3091  fun2ssres  5230  fcoi1  5367  fcoi2  5368  funssfv  5511  caovimo  6031  mpomptsx  6162  dmmpossx  6164  fmpox  6165  2ndconst  6186  mpoxopoveq  6204  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  rdgivallem  6345  nnmass  6451  nnm00  6493  ssenen  6813  fi0  6936  nnnninf2  7087  nnnninfeq2  7089  exmidfodomrlemim  7153  ltexnqq  7345  ltrnqg  7357  nqnq0a  7391  nqnq0m  7392  nq0m0r  7393  nq0a0  7394  addnqprllem  7464  addnqprulem  7465  map2psrprg  7742  rereceu  7826  addid0  8267  nnnn0addcl  9140  zindd  9305  qaddcl  9569  qmulcl  9571  qreccl  9576  xaddpnf1  9778  xaddmnf1  9780  xaddnemnf  9789  xaddnepnf  9790  xaddcom  9793  xnegdi  9800  xaddass  9801  xpncan  9803  xleadd1a  9805  xltadd1  9808  xlt2add  9812  modfzo0difsn  10326  frec2uzrdg  10340  expp1  10458  expnegap0  10459  expcllem  10462  mulexp  10490  expmul  10496  sqoddm1div8  10604  bcpasc  10675  hashfzo  10731  shftfn  10762  reim0b  10800  cjexp  10831  sumsnf  11346  binomlem  11420  prodsnf  11529  ef0lem  11597  dvdsnegb  11744  m1expe  11832  m1expo  11833  m1exp1  11834  flodddiv4  11867  gcdabs  11917  bezoutr1  11962  dvdslcm  11997  lcmeq0  11999  lcmcl  12000  lcmabs  12004  lcmgcdlem  12005  lcmdvds  12007  mulgcddvds  12022  qredeu  12025  divgcdcoprmex  12030  pcge0  12240  pcgcd1  12255  pcadd  12267  pcmpt2  12270  isxmet2d  12948  blfvalps  12985  blssioo  13145  efper  13328  relogbcxpbap  13483  logbgcd1irr  13485  lgsdir  13536  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  trirec0xor  13884