Theorem sylan9eqr 2248

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 2246	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  sbcied2  3023  csbied2  3128  fun2ssres  5297  fcoi1  5434  fcoi2  5435  funssfv  5580  caovimo  6112  mpomptsx  6250  dmmpossx  6252  fmpox  6253  2ndconst  6275  mpoxopoveq  6293  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  rdgivallem  6434  nnmass  6540  nnm00  6583  ssenen  6907  fi0  7034  nnnninf2  7186  nnnninfeq2  7188  exmidfodomrlemim  7261  ltexnqq  7468  ltrnqg  7480  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  nq0a0  7517  addnqprllem  7587  addnqprulem  7588  map2psrprg  7865  rereceu  7949  addid0  8392  nnnn0addcl  9270  zindd  9435  qaddcl  9700  qmulcl  9702  qreccl  9707  xaddpnf1  9912  xaddmnf1  9914  xaddnemnf  9923  xaddnepnf  9924  xaddcom  9927  xnegdi  9934  xaddass  9935  xpncan  9937  xleadd1a  9939  xltadd1  9942  xlt2add  9946  modfzo0difsn  10466  frec2uzrdg  10480  seqf1oglem2  10591  expp1  10617  expnegap0  10618  expcllem  10621  mulexp  10649  expmul  10655  sqoddm1div8  10764  bcpasc  10837  hashfzo  10893  shftfn  10968  reim0b  11006  cjexp  11037  sumsnf  11552  binomlem  11626  prodsnf  11735  ef0lem  11803  dvdsnegb  11951  m1expe  12040  m1expo  12041  m1exp1  12042  flodddiv4  12075  gcdabs  12125  bezoutr1  12170  dvdslcm  12207  lcmeq0  12209  lcmcl  12210  lcmabs  12214  lcmgcdlem  12215  lcmdvds  12217  mulgcddvds  12232  qredeu  12235  divgcdcoprmex  12240  pcge0  12451  pcgcd1  12466  pcadd  12478  pcmpt2  12482  mulgfvalg  13191  mulgnn0subcl  13205  mulgnn0z  13219  f1ghm0to0  13342  srgmulgass  13485  srgpcomp  13486  ringinvnzdiv  13546  lmodvsmmulgdi  13819  znval  14124  isxmet2d  14516  blfvalps  14553  blssioo  14713  efper  14942  relogbcxpbap  15097  logbgcd1irr  15099  lgsdir  15151  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  trirec0xor  15535