Theorem sylan9eqr 2230

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

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

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  sbcied2  2998  csbied2  3102  fun2ssres  5251  fcoi1  5388  fcoi2  5389  funssfv  5533  caovimo  6058  mpomptsx  6188  dmmpossx  6190  fmpox  6191  2ndconst  6213  mpoxopoveq  6231  tfrlemisucaccv  6316  tfr1onlemsucaccv  6332  tfrcllemsucaccv  6345  rdgivallem  6372  nnmass  6478  nnm00  6521  ssenen  6841  fi0  6964  nnnninf2  7115  nnnninfeq2  7117  exmidfodomrlemim  7190  ltexnqq  7382  ltrnqg  7394  nqnq0a  7428  nqnq0m  7429  nq0m0r  7430  nq0a0  7431  addnqprllem  7501  addnqprulem  7502  map2psrprg  7779  rereceu  7863  addid0  8304  nnnn0addcl  9179  zindd  9344  qaddcl  9608  qmulcl  9610  qreccl  9615  xaddpnf1  9817  xaddmnf1  9819  xaddnemnf  9828  xaddnepnf  9829  xaddcom  9832  xnegdi  9839  xaddass  9840  xpncan  9842  xleadd1a  9844  xltadd1  9847  xlt2add  9851  modfzo0difsn  10365  frec2uzrdg  10379  expp1  10497  expnegap0  10498  expcllem  10501  mulexp  10529  expmul  10535  sqoddm1div8  10643  bcpasc  10714  hashfzo  10770  shftfn  10801  reim0b  10839  cjexp  10870  sumsnf  11385  binomlem  11459  prodsnf  11568  ef0lem  11636  dvdsnegb  11783  m1expe  11871  m1expo  11872  m1exp1  11873  flodddiv4  11906  gcdabs  11956  bezoutr1  12001  dvdslcm  12036  lcmeq0  12038  lcmcl  12039  lcmabs  12043  lcmgcdlem  12044  lcmdvds  12046  mulgcddvds  12061  qredeu  12064  divgcdcoprmex  12069  pcge0  12279  pcgcd1  12294  pcadd  12306  pcmpt2  12309  mulgfvalg  12855  mulgnn0subcl  12866  mulgnn0z  12879  srgmulgass  12978  srgpcomp  12979  ringinvnzdiv  13032  isxmet2d  13428  blfvalps  13465  blssioo  13625  efper  13808  relogbcxpbap  13963  logbgcd1irr  13965  lgsdir  14016  lgsne0  14019  lgsdirnn0  14028  lgsdinn0  14029  trirec0xor  14363