MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9req Structured version   Visualization version   GIF version

Theorem sylan9req 2664
Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
Hypotheses
Ref Expression
sylan9req.1 (𝜑𝐵 = 𝐴)
sylan9req.2 (𝜓𝐵 = 𝐶)
Assertion
Ref Expression
sylan9req ((𝜑𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9req
StepHypRef Expression
1 sylan9req.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2615 . 2 (𝜑𝐴 = 𝐵)
3 sylan9req.2 . 2 (𝜓𝐵 = 𝐶)
42, 3sylan9eq 2663 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602
This theorem is referenced by:  ordintdif  5676  fndmu  5891  fodmrnu  6020  funcoeqres  6064  tz7.44-3  7368  dfac5lem4  8809  zdiv  11281  hashimarni  13040  ccatws1lenrev  13208  fprodss  14465  dvdsmulc  14795  smumullem  15000  cncongrcoprm  15170  mgmidmo  17030  reslmhm2b  18823  fclsfnflim  21588  ustuqtop1  21802  ulm2  23887  sineq0  24021  cxple2a  24189  sqff1o  24652  lgsmodeq  24811  eedimeq  25523  grpoidinvlem4  26538  hlimuni  27272  dmdsl3  28351  atoml2i  28419  disjpreima  28572  sspreima  28620  xrge0npcan  28818  poimirlem3  32365  poimirlem4  32366  poimirlem16  32378  poimirlem17  32379  poimirlem19  32381  poimirlem20  32382  poimirlem23  32385  poimirlem24  32386  poimirlem25  32387  poimirlem29  32391  poimirlem31  32393  eqfnun  32469  ltrncnvnid  34214  cdleme20j  34407  cdleme42ke  34574  dia2dimlem13  35166  dvh4dimN  35537  mapdval4N  35722  sineq0ALT  37978  cncfiooicc  38563  fourierdlem41  38824  fourierdlem71  38853  bgoldbtbndlem4  40008  bgoldbtbnd  40009
  Copyright terms: Public domain W3C validator