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

Theorem syl6reqr 2167
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1 (𝜑𝐴 = 𝐵)
syl6reqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6reqr (𝜑𝐶 = 𝐴)

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6reqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2119 . 2 𝐵 = 𝐶
41, 3syl6req 2165 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1314 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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-cleq 2108 This theorem is referenced by:  iftrue  3447  iffalse  3450  difprsn1  3627  dmmptg  5004  relcoi1  5038  funimacnv  5167  dmmptd  5221  dffv3g  5383  dfimafn  5436  fvco2  5456  isoini  5685  oprabco  6080  ixpconstg  6567  unfiexmid  6772  undifdc  6778  sbthlemi4  6814  sbthlemi5  6815  sbthlemi6  6816  supval2ti  6848  exmidfodomrlemim  7021  suplocexprlemex  7494  eqneg  8455  zeo  9110  fseq1p1m1  9825  seq3val  10182  seqvalcd  10183  hashfzo  10519  hashxp  10523  fsumconst  11174  modfsummod  11178  telfsumo  11186  mulgcd  11611  algcvg  11636  phiprmpw  11804  strslfv3  11910  uptx  12349  resubmet  12623
 Copyright terms: Public domain W3C validator