Theorem sylan9eqr 2135

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

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  sbcied2  2851  csbied2  2949  fun2ssres  4963  fcoi1  5090  fcoi2  5091  funssfv  5220  caovimo  5714  mpt2mptsx  5843  dmmpt2ssx  5845  fmpt2x  5846  2ndconst  5863  mpt2xopoveq  5878  tfrlemisucaccv  5962  rdgivallem  5991  nnmass  6089  nnm00  6125  ltexnqq  6598  ltrnqg  6610  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  nq0a0  6647  addnqprllem  6717  addnqprulem  6718  rereceu  7055  addid0  7477  nnnn0addcl  8318  zindd  8465  qaddcl  8720  qmulcl  8722  qreccl  8727  modfzo0difsn  9397  frec2uzrdg  9411  expp1  9483  expnegap0  9484  expcllem  9487  mulexp  9515  expmul  9521  sqoddm1div8  9625  bcpasc  9693  shftfn  9712  reim0b  9749  cjexp  9780  dvdsnegb  10212  m1expe  10299  m1expo  10300  m1exp1  10301  flodddiv4  10334  gcdabs  10379  bezoutr1  10422  dvdslcm  10451  lcmeq0  10453  lcmcl  10454  lcmabs  10458  lcmgcdlem  10459  lcmdvds  10461  mulgcddvds  10476  qredeu  10479  divgcdcoprmex  10484