Theorem sylan9eqr 2284

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  sbcied2  3066  csbied2  3172  fun2ssres  5364  fcoi1  5511  fcoi2  5512  funssfv  5658  caovimo  6208  mpomptsx  6354  dmmpossx  6356  fmpox  6357  2ndconst  6379  mpoxopoveq  6397  tfrlemisucaccv  6482  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  rdgivallem  6538  nnmass  6646  nnm00  6689  ssenen  7025  fi0  7158  nnnninf2  7310  nnnninfeq2  7312  exmidfodomrlemim  7395  ltexnqq  7611  ltrnqg  7623  nqnq0a  7657  nqnq0m  7658  nq0m0r  7659  nq0a0  7660  addnqprllem  7730  addnqprulem  7731  map2psrprg  8008  rereceu  8092  addid0  8535  nnnn0addcl  9415  zindd  9581  qaddcl  9847  qmulcl  9849  qreccl  9854  xaddpnf1  10059  xaddmnf1  10061  xaddnemnf  10070  xaddnepnf  10071  xaddcom  10074  xnegdi  10081  xaddass  10082  xpncan  10084  xleadd1a  10086  xltadd1  10089  xlt2add  10093  modfzo0difsn  10634  frec2uzrdg  10648  seqf1oglem2  10759  expp1  10785  expnegap0  10786  expcllem  10789  mulexp  10817  expmul  10823  sqoddm1div8  10932  bcpasc  11005  hashfzo  11062  lsw0  11137  ccatval1  11150  ccatval2  11151  swrdval  11201  ccatopth  11269  reuccatpfxs1  11300  shftfn  11356  reim0b  11394  cjexp  11425  sumsnf  11941  binomlem  12015  prodsnf  12124  ef0lem  12192  dvdsnegb  12340  m1expe  12431  m1expo  12432  m1exp1  12433  flodddiv4  12468  gcdabs  12530  bezoutr1  12575  dvdslcm  12612  lcmeq0  12614  lcmcl  12615  lcmabs  12619  lcmgcdlem  12620  lcmdvds  12622  mulgcddvds  12637  qredeu  12640  divgcdcoprmex  12645  pcge0  12857  pcgcd1  12872  pcadd  12884  pcmpt2  12888  mulgfvalg  13679  mulgnn0subcl  13693  mulgnn0z  13707  f1ghm0to0  13830  srgmulgass  13973  srgpcomp  13974  ringinvnzdiv  14034  lmodvsmmulgdi  14308  znval  14621  mplvalcoe  14675  isxmet2d  15043  blfvalps  15080  blssioo  15248  efper  15502  relogbcxpbap  15660  logbgcd1irr  15662  lgsdir  15735  lgsne0  15738  lgsdirnn0  15747  lgsdinn0  15748  lgsquadlem2  15778  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  wlklenvm1  16113  wlklenvm1g  16114  wlk0prc  16144  clwwlkn2  16189  trirec0xor  16527