Theorem sylan9eqr 2287

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  sbcied2  3079  csbied2  3185  fun2ssres  5395  fcoi1  5546  fcoi2  5547  funssfv  5695  caovimo  6247  mpomptsx  6392  dmmpossx  6394  fmpox  6395  2ndconst  6417  mpoxopoveq  6470  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  rdgivallem  6611  nnmass  6719  nnm00  6762  mapsnend  7051  ssenen  7104  fi0  7261  nnnninf2  7417  nnnninfeq2  7419  exmidfodomrlemim  7503  ltexnqq  7722  ltrnqg  7734  nqnq0a  7768  nqnq0m  7769  nq0m0r  7770  nq0a0  7771  addnqprllem  7841  addnqprulem  7842  map2psrprg  8119  rereceu  8203  addid0  8645  nnnn0addcl  9525  zindd  9695  qaddcl  9966  qmulcl  9968  qreccl  9973  xaddpnf1  10178  xaddmnf1  10180  xaddnemnf  10189  xaddnepnf  10190  xaddcom  10193  xnegdi  10200  xaddass  10201  xpncan  10203  xleadd1a  10205  xltadd1  10208  xlt2add  10212  modfzo0difsn  10756  frec2uzrdg  10770  seqf1oglem2  10881  expp1  10907  expnegap0  10908  expcllem  10911  mulexp  10939  expmul  10945  sqoddm1div8  11054  bcpasc  11127  hashfzo  11185  lsw0  11268  ccatval1  11281  ccatval2  11282  swrdval  11336  ccatopth  11404  reuccatpfxs1  11435  shftfn  11505  reim0b  11543  cjexp  11574  sumsnf  12091  binomlem  12165  prodsnf  12274  ef0lem  12342  dvdsnegb  12490  m1expe  12581  m1expo  12582  m1exp1  12583  flodddiv4  12618  gcdabs  12680  bezoutr1  12725  dvdslcm  12762  lcmeq0  12764  lcmcl  12765  lcmabs  12769  lcmgcdlem  12770  lcmdvds  12772  mulgcddvds  12787  qredeu  12790  divgcdcoprmex  12795  pcge0  13007  pcgcd1  13022  pcadd  13034  pcmpt2  13038  mulgfvalg  13830  mulgnn0subcl  13844  mulgnn0z  13858  f1ghm0to0  13981  srgmulgass  14125  srgpcomp  14126  ringinvnzdiv  14186  lmodvsmmulgdi  14463  znval  14776  mplvalcoe  14837  isxmet2d  15205  blfvalps  15242  blssioo  15410  efper  15664  relogbcxpbap  15822  logbgcd1irr  15824  lgsdir  15900  lgsne0  15903  lgsdirnn0  15912  lgsdinn0  15913  lgsquadlem2  15943  2lgslem3a  15958  2lgslem3b  15959  2lgslem3c  15960  2lgslem3d  15961  2lgslem3a1  15962  2lgslem3b1  15963  2lgslem3c1  15964  2lgslem3d1  15965  wlklenvm1  16328  wlklenvm1g  16329  wlk0prc  16359  clwwlkn2  16408  trirec0xor  16821