Theorem sylan9eqr 2149

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

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

This theorem is referenced by:  sbcied2  2890  csbied2  2989  fun2ssres  5091  fcoi1  5226  fcoi2  5227  funssfv  5365  caovimo  5876  mpt2mptsx  6005  dmmpt2ssx  6007  fmpt2x  6008  2ndconst  6025  mpt2xopoveq  6043  tfrlemisucaccv  6128  tfr1onlemsucaccv  6144  tfrcllemsucaccv  6157  rdgivallem  6184  nnmass  6288  nnm00  6328  ssenen  6647  exmidfodomrlemim  6924  ltexnqq  7064  ltrnqg  7076  nqnq0a  7110  nqnq0m  7111  nq0m0r  7112  nq0a0  7113  addnqprllem  7183  addnqprulem  7184  rereceu  7521  addid0  7948  nnnn0addcl  8801  zindd  8963  qaddcl  9219  qmulcl  9221  qreccl  9226  xaddpnf1  9412  xaddmnf1  9414  xaddnemnf  9423  xaddnepnf  9424  xaddcom  9427  xnegdi  9434  xaddass  9435  xpncan  9437  xleadd1a  9439  xltadd1  9442  xlt2add  9446  modfzo0difsn  9951  frec2uzrdg  9965  expp1  10077  expnegap0  10078  expcllem  10081  mulexp  10109  expmul  10115  sqoddm1div8  10221  bcpasc  10289  hashfzo  10345  shftfn  10373  reim0b  10411  cjexp  10442  sumsnf  10952  binomlem  11026  ef0lem  11099  dvdsnegb  11240  m1expe  11326  m1expo  11327  m1exp1  11328  flodddiv4  11361  gcdabs  11406  bezoutr1  11449  dvdslcm  11478  lcmeq0  11480  lcmcl  11481  lcmabs  11485  lcmgcdlem  11486  lcmdvds  11488  mulgcddvds  11503  qredeu  11506  divgcdcoprmex  11511  isxmet2d  12134  blfvalps  12171  blssioo  12319