Theorem sylan9eqr 2251

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  sbcied2  3027  csbied2  3132  fun2ssres  5301  fcoi1  5438  fcoi2  5439  funssfv  5584  caovimo  6117  mpomptsx  6255  dmmpossx  6257  fmpox  6258  2ndconst  6280  mpoxopoveq  6298  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  rdgivallem  6439  nnmass  6545  nnm00  6588  ssenen  6912  fi0  7041  nnnninf2  7193  nnnninfeq2  7195  exmidfodomrlemim  7268  ltexnqq  7475  ltrnqg  7487  nqnq0a  7521  nqnq0m  7522  nq0m0r  7523  nq0a0  7524  addnqprllem  7594  addnqprulem  7595  map2psrprg  7872  rereceu  7956  addid0  8399  nnnn0addcl  9279  zindd  9444  qaddcl  9709  qmulcl  9711  qreccl  9716  xaddpnf1  9921  xaddmnf1  9923  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xnegdi  9943  xaddass  9944  xpncan  9946  xleadd1a  9948  xltadd1  9951  xlt2add  9955  modfzo0difsn  10487  frec2uzrdg  10501  seqf1oglem2  10612  expp1  10638  expnegap0  10639  expcllem  10642  mulexp  10670  expmul  10676  sqoddm1div8  10785  bcpasc  10858  hashfzo  10914  shftfn  10989  reim0b  11027  cjexp  11058  sumsnf  11574  binomlem  11648  prodsnf  11757  ef0lem  11825  dvdsnegb  11973  m1expe  12064  m1expo  12065  m1exp1  12066  flodddiv4  12101  gcdabs  12155  bezoutr1  12200  dvdslcm  12237  lcmeq0  12239  lcmcl  12240  lcmabs  12244  lcmgcdlem  12245  lcmdvds  12247  mulgcddvds  12262  qredeu  12265  divgcdcoprmex  12270  pcge0  12482  pcgcd1  12497  pcadd  12509  pcmpt2  12513  mulgfvalg  13251  mulgnn0subcl  13265  mulgnn0z  13279  f1ghm0to0  13402  srgmulgass  13545  srgpcomp  13546  ringinvnzdiv  13606  lmodvsmmulgdi  13879  znval  14192  isxmet2d  14584  blfvalps  14621  blssioo  14789  efper  15043  relogbcxpbap  15201  logbgcd1irr  15203  lgsdir  15276  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  lgsquadlem2  15319  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  trirec0xor  15689