Theorem sylan9eqr 2194

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  sbcied2  2946  csbied2  3047  fun2ssres  5166  fcoi1  5303  fcoi2  5304  funssfv  5447  caovimo  5964  mpomptsx  6095  dmmpossx  6097  fmpox  6098  2ndconst  6119  mpoxopoveq  6137  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  rdgivallem  6278  nnmass  6383  nnm00  6425  ssenen  6745  fi0  6863  exmidfodomrlemim  7057  ltexnqq  7216  ltrnqg  7228  nqnq0a  7262  nqnq0m  7263  nq0m0r  7264  nq0a0  7265  addnqprllem  7335  addnqprulem  7336  map2psrprg  7613  rereceu  7697  addid0  8135  nnnn0addcl  9007  zindd  9169  qaddcl  9427  qmulcl  9429  qreccl  9434  xaddpnf1  9629  xaddmnf1  9631  xaddnemnf  9640  xaddnepnf  9641  xaddcom  9644  xnegdi  9651  xaddass  9652  xpncan  9654  xleadd1a  9656  xltadd1  9659  xlt2add  9663  modfzo0difsn  10168  frec2uzrdg  10182  expp1  10300  expnegap0  10301  expcllem  10304  mulexp  10332  expmul  10338  sqoddm1div8  10444  bcpasc  10512  hashfzo  10568  shftfn  10596  reim0b  10634  cjexp  10665  sumsnf  11178  binomlem  11252  ef0lem  11366  dvdsnegb  11510  m1expe  11596  m1expo  11597  m1exp1  11598  flodddiv4  11631  gcdabs  11676  bezoutr1  11721  dvdslcm  11750  lcmeq0  11752  lcmcl  11753  lcmabs  11757  lcmgcdlem  11758  lcmdvds  11760  mulgcddvds  11775  qredeu  11778  divgcdcoprmex  11783  isxmet2d  12517  blfvalps  12554  blssioo  12714  efper  12888