Theorem sylan9eqr 2225

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

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

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  sbcied2  2992  csbied2  3096  fun2ssres  5241  fcoi1  5378  fcoi2  5379  funssfv  5522  caovimo  6046  mpomptsx  6176  dmmpossx  6178  fmpox  6179  2ndconst  6201  mpoxopoveq  6219  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  rdgivallem  6360  nnmass  6466  nnm00  6509  ssenen  6829  fi0  6952  nnnninf2  7103  nnnninfeq2  7105  exmidfodomrlemim  7178  ltexnqq  7370  ltrnqg  7382  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  nq0a0  7419  addnqprllem  7489  addnqprulem  7490  map2psrprg  7767  rereceu  7851  addid0  8292  nnnn0addcl  9165  zindd  9330  qaddcl  9594  qmulcl  9596  qreccl  9601  xaddpnf1  9803  xaddmnf1  9805  xaddnemnf  9814  xaddnepnf  9815  xaddcom  9818  xnegdi  9825  xaddass  9826  xpncan  9828  xleadd1a  9830  xltadd1  9833  xlt2add  9837  modfzo0difsn  10351  frec2uzrdg  10365  expp1  10483  expnegap0  10484  expcllem  10487  mulexp  10515  expmul  10521  sqoddm1div8  10629  bcpasc  10700  hashfzo  10757  shftfn  10788  reim0b  10826  cjexp  10857  sumsnf  11372  binomlem  11446  prodsnf  11555  ef0lem  11623  dvdsnegb  11770  m1expe  11858  m1expo  11859  m1exp1  11860  flodddiv4  11893  gcdabs  11943  bezoutr1  11988  dvdslcm  12023  lcmeq0  12025  lcmcl  12026  lcmabs  12030  lcmgcdlem  12031  lcmdvds  12033  mulgcddvds  12048  qredeu  12051  divgcdcoprmex  12056  pcge0  12266  pcgcd1  12281  pcadd  12293  pcmpt2  12296  isxmet2d  13142  blfvalps  13179  blssioo  13339  efper  13522  relogbcxpbap  13677  logbgcd1irr  13679  lgsdir  13730  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  trirec0xor  14077