ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9eqr GIF version

Theorem sylan9eqr 2248
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
StepHypRef Expression
1 sylan9eqr.1 . . 3 (𝜑𝐴 = 𝐵)
2 sylan9eqr.2 . . 3 (𝜓𝐵 = 𝐶)
31, 2sylan9eq 2246 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 268 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1364
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-cleq 2186
This theorem is referenced by:  sbcied2  3024  csbied2  3129  fun2ssres  5298  fcoi1  5435  fcoi2  5436  funssfv  5581  caovimo  6114  mpomptsx  6252  dmmpossx  6254  fmpox  6255  2ndconst  6277  mpoxopoveq  6295  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  rdgivallem  6436  nnmass  6542  nnm00  6585  ssenen  6909  fi0  7036  nnnninf2  7188  nnnninfeq2  7190  exmidfodomrlemim  7263  ltexnqq  7470  ltrnqg  7482  nqnq0a  7516  nqnq0m  7517  nq0m0r  7518  nq0a0  7519  addnqprllem  7589  addnqprulem  7590  map2psrprg  7867  rereceu  7951  addid0  8394  nnnn0addcl  9273  zindd  9438  qaddcl  9703  qmulcl  9705  qreccl  9710  xaddpnf1  9915  xaddmnf1  9917  xaddnemnf  9926  xaddnepnf  9927  xaddcom  9930  xnegdi  9937  xaddass  9938  xpncan  9940  xleadd1a  9942  xltadd1  9945  xlt2add  9949  modfzo0difsn  10469  frec2uzrdg  10483  seqf1oglem2  10594  expp1  10620  expnegap0  10621  expcllem  10624  mulexp  10652  expmul  10658  sqoddm1div8  10767  bcpasc  10840  hashfzo  10896  shftfn  10971  reim0b  11009  cjexp  11040  sumsnf  11555  binomlem  11629  prodsnf  11738  ef0lem  11806  dvdsnegb  11954  m1expe  12043  m1expo  12044  m1exp1  12045  flodddiv4  12078  gcdabs  12128  bezoutr1  12173  dvdslcm  12210  lcmeq0  12212  lcmcl  12213  lcmabs  12217  lcmgcdlem  12218  lcmdvds  12220  mulgcddvds  12235  qredeu  12238  divgcdcoprmex  12243  pcge0  12454  pcgcd1  12469  pcadd  12481  pcmpt2  12485  mulgfvalg  13194  mulgnn0subcl  13208  mulgnn0z  13222  f1ghm0to0  13345  srgmulgass  13488  srgpcomp  13489  ringinvnzdiv  13549  lmodvsmmulgdi  13822  znval  14135  isxmet2d  14527  blfvalps  14564  blssioo  14732  efper  14983  relogbcxpbap  15138  logbgcd1irr  15140  lgsdir  15192  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  lgsquadlem2  15235  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  trirec0xor  15605
  Copyright terms: Public domain W3C validator