Theorem sylan9eqr 2195

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

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

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  sbcied2  2950  csbied2  3052  fun2ssres  5174  fcoi1  5311  fcoi2  5312  funssfv  5455  caovimo  5972  mpomptsx  6103  dmmpossx  6105  fmpox  6106  2ndconst  6127  mpoxopoveq  6145  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  rdgivallem  6286  nnmass  6391  nnm00  6433  ssenen  6753  fi0  6871  exmidfodomrlemim  7074  ltexnqq  7240  ltrnqg  7252  nqnq0a  7286  nqnq0m  7287  nq0m0r  7288  nq0a0  7289  addnqprllem  7359  addnqprulem  7360  map2psrprg  7637  rereceu  7721  addid0  8159  nnnn0addcl  9031  zindd  9193  qaddcl  9454  qmulcl  9456  qreccl  9461  xaddpnf1  9659  xaddmnf1  9661  xaddnemnf  9670  xaddnepnf  9671  xaddcom  9674  xnegdi  9681  xaddass  9682  xpncan  9684  xleadd1a  9686  xltadd1  9689  xlt2add  9693  modfzo0difsn  10199  frec2uzrdg  10213  expp1  10331  expnegap0  10332  expcllem  10335  mulexp  10363  expmul  10369  sqoddm1div8  10475  bcpasc  10544  hashfzo  10600  shftfn  10628  reim0b  10666  cjexp  10697  sumsnf  11210  binomlem  11284  ef0lem  11403  dvdsnegb  11546  m1expe  11632  m1expo  11633  m1exp1  11634  flodddiv4  11667  gcdabs  11712  bezoutr1  11757  dvdslcm  11786  lcmeq0  11788  lcmcl  11789  lcmabs  11793  lcmgcdlem  11794  lcmdvds  11796  mulgcddvds  11811  qredeu  11814  divgcdcoprmex  11819  isxmet2d  12556  blfvalps  12593  blssioo  12753  efper  12936  relogbcxpbap  13090  logbgcd1irr  13092  trirec0xor  13413