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

Theorem syl6eqr 2190
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eqr.1 (𝜑𝐴 = 𝐵)
syl6eqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6eqr (𝜑𝐴 = 𝐶)

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2143 . 2 𝐵 = 𝐶
41, 3syl6eq 2188 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  3eqtr4g  2197  rabxmdc  3394  relop  4689  csbcnvg  4723  dfiun3g  4796  dfiin3g  4797  resima2  4853  relcnvfld  5072  uniabio  5098  fntpg  5179  dffn5im  5467  dfimafn2  5471  fncnvima2  5541  fmptcof  5587  fcoconst  5591  fnasrng  5600  ffnov  5875  fnovim  5879  fnrnov  5916  foov  5917  funimassov  5920  ovelimab  5921  ofc12  6002  caofinvl  6004  dftpos3  6159  tfr0dm  6219  rdgisucinc  6282  oasuc  6360  ecinxp  6504  phplem1  6746  exmidpw  6802  unfiin  6814  fidcenumlemr  6843  0ct  6992  ctmlemr  6993  exmidaclem  7069  indpi  7162  nqnq0pi  7258  nq0m0r  7276  addnqpr1  7382  recexgt0sr  7593  suplocsrlempr  7627  recidpipr  7676  recidpirq  7678  axrnegex  7699  nntopi  7714  cnref1o  9452  fztp  9870  fseq1m1p1  9887  frecuzrdgrrn  10193  frecuzrdgsuc  10199  frecuzrdgsuctlem  10208  seq3val  10243  seqvalcd  10244  fser0const  10301  mulexpzap  10345  expaddzap  10349  bcp1m1  10523  cjexp  10677  rexuz3  10774  bdtri  11023  climconst  11071  sumfct  11155  zsumdc  11165  fsum3  11168  sum0  11169  fsumcnv  11218  mertenslem2  11317  ef0lem  11378  efzval  11401  efival  11450  sinbnd  11470  cosbnd  11471  eucalgval  11746  eucalginv  11748  eucalglt  11749  eucalgcvga  11750  eucalg  11751  sqpweven  11864  2sqpwodd  11865  dfphi2  11907  phimullem  11912  ennnfonelemhdmp1  11933  ennnfonelemkh  11936  ressid2  12032  ressval2  12033  topnvalg  12146  istps  12213  cldval  12282  ntrfval  12283  clsfval  12284  neifval  12323  restbasg  12351  tgrest  12352  txval  12438  upxp  12455  uptx  12457  txrest  12459  lmcn2  12463  cnmpt2t  12476  cnmpt2res  12480  imasnopn  12482  psmetxrge0  12515  xmetge0  12548  isxms  12634  isms  12636  bdxmet  12684  qtopbasss  12704  cnblcld  12718  negfcncf  12772  dvfvalap  12833  eldvap  12834  dvidlemap  12843  dvexp2  12859  dvrecap  12860  dveflem  12870  sin0pilem1  12884  ptolemy  12927  coskpi  12951  nninfsellemqall  13272
  Copyright terms: Public domain W3C validator