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

Theorem syl6reqr 2091
 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 2044 . 2 𝐵 = 𝐶
41, 3syl6req 2089 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  iftrue  3336  iffalse  3339  difprsn1  3503  dmmptg  4818  relcoi1  4849  funimacnv  4975  dffv3g  5174  dfimafn  5222  fvco2  5242  isoini  5457  oprabco  5838  eqneg  7708  zeo  8343  fseq1p1m1  8956  iseqval  9220  ialgrp1  9885  ialgcvg  9887
 Copyright terms: Public domain W3C validator