Theorem sylan9eqr 2293

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  sbcied2  3089  csbied2  3195  fun2ssres  5419  fcoi1  5570  fcoi2  5571  funssfv  5719  caovimo  6277  mpomptsx  6427  dmmpossx  6429  fmpox  6430  2ndconst  6452  mpoxopoveq  6505  tfrlemisucaccv  6590  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  rdgivallem  6646  nnmass  6754  nnm00  6797  mapsnend  7093  ssenen  7146  fi0  7303  nnnninf2  7461  nnnninfeq2  7463  exmidfodomrlemim  7547  ltexnqq  7769  ltrnqg  7781  nqnq0a  7815  nqnq0m  7816  nq0m0r  7817  nq0a0  7818  addnqprllem  7888  addnqprulem  7889  map2psrprg  8166  rereceu  8250  addid0  8693  nnnn0addcl  9576  zindd  9747  qaddcl  10018  qmulcl  10020  qreccl  10025  xaddpnf1  10231  xaddmnf1  10233  xaddnemnf  10242  xaddnepnf  10243  xaddcom  10246  xnegdi  10253  xaddass  10254  xpncan  10256  xleadd1a  10258  xltadd1  10261  xlt2add  10265  modfzo0difsn  10815  frec2uzrdg  10829  seqf1oglem2  10940  expp1  10966  expnegap0  10967  expcllem  10970  mulexp  10998  expmul  11004  sqoddm1div8  11114  bcpasc  11187  hashfzo  11246  hashf1lem1  11268  lsw0  11335  ccatval1  11348  ccatval2  11349  swrdval  11403  ccatopth  11471  reuccatpfxs1  11502  shftfn  11572  reim0b  11610  cjexp  11641  sumsnf  12159  binomlem  12233  prodsnf  12342  ef0lem  12410  dvdsnegb  12558  m1expe  12649  m1expo  12650  m1exp1  12651  flodddiv4  12686  gcdabs  12748  bezoutr1  12793  dvdslcm  12830  lcmeq0  12832  lcmcl  12833  lcmabs  12837  lcmgcdlem  12838  lcmdvds  12840  mulgcddvds  12855  qredeu  12858  divgcdcoprmex  12863  pcge0  13075  pcgcd1  13090  pcadd  13102  pcmpt2  13106  mulgfvalg  13907  mulgnn0subcl  13921  mulgnn0z  13935  f1ghm0to0  14058  srgmulgass  14276  srgpcomp  14277  ringinvnzdiv  14338  lmodvsmmulgdi  14643  znval  14954  assamulgscmlem2  15025  mplvalcoe  15064  isxmet2d  15432  blfvalps  15469  blssioo  15637  efper  15891  relogbcxpbap  16050  logbgcd1irr  16052  lgsdir  16137  lgsne0  16140  lgsdirnn0  16149  lgsdinn0  16150  lgsquadlem2  16180  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  wlklenvm1  16565  wlklenvm1g  16566  wlk0prc  16596  clwwlkn2  16645  trirec0xor  17068