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  5361  fcoi1  5508  fcoi2  5509  funssfv  5655  caovimo  6205  mpomptsx  6349  dmmpossx  6351  fmpox  6352  2ndconst  6374  mpoxopoveq  6392  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  rdgivallem  6533  nnmass  6641  nnm00  6684  ssenen  7020  fi0  7150  nnnninf2  7302  nnnninfeq2  7304  exmidfodomrlemim  7387  ltexnqq  7603  ltrnqg  7615  nqnq0a  7649  nqnq0m  7650  nq0m0r  7651  nq0a0  7652  addnqprllem  7722  addnqprulem  7723  map2psrprg  8000  rereceu  8084  addid0  8527  nnnn0addcl  9407  zindd  9573  qaddcl  9838  qmulcl  9840  qreccl  9845  xaddpnf1  10050  xaddmnf1  10052  xaddnemnf  10061  xaddnepnf  10062  xaddcom  10065  xnegdi  10072  xaddass  10073  xpncan  10075  xleadd1a  10077  xltadd1  10080  xlt2add  10084  modfzo0difsn  10625  frec2uzrdg  10639  seqf1oglem2  10750  expp1  10776  expnegap0  10777  expcllem  10780  mulexp  10808  expmul  10814  sqoddm1div8  10923  bcpasc  10996  hashfzo  11052  lsw0  11127  ccatval1  11140  ccatval2  11141  swrdval  11188  ccatopth  11256  reuccatpfxs1  11287  shftfn  11343  reim0b  11381  cjexp  11412  sumsnf  11928  binomlem  12002  prodsnf  12111  ef0lem  12179  dvdsnegb  12327  m1expe  12418  m1expo  12419  m1exp1  12420  flodddiv4  12455  gcdabs  12517  bezoutr1  12562  dvdslcm  12599  lcmeq0  12601  lcmcl  12602  lcmabs  12606  lcmgcdlem  12607  lcmdvds  12609  mulgcddvds  12624  qredeu  12627  divgcdcoprmex  12632  pcge0  12844  pcgcd1  12859  pcadd  12871  pcmpt2  12875  mulgfvalg  13666  mulgnn0subcl  13680  mulgnn0z  13694  f1ghm0to0  13817  srgmulgass  13960  srgpcomp  13961  ringinvnzdiv  14021  lmodvsmmulgdi  14295  znval  14608  mplvalcoe  14662  isxmet2d  15030  blfvalps  15067  blssioo  15235  efper  15489  relogbcxpbap  15647  logbgcd1irr  15649  lgsdir  15722  lgsne0  15725  lgsdirnn0  15734  lgsdinn0  15735  lgsquadlem2  15765  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787  wlklenvm1  16062  wlklenvm1g  16063  wlk0prc  16093  trirec0xor  16443