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

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

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2143 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2185 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:  bm2.5ii  4412  resdmdfsn  4862  f0dom0  5316  f1o00  5402  fmpt  5570  fmptsn  5609  resfunexg  5641  mapsn  6584  sbthlemi4  6848  sbthlemi6  6850  pm54.43  7046  prarloclem5  7315  recexprlem1ssl  7448  recexprlem1ssu  7449  iooval2  9705  hashsng  10551  zfz1isolem1  10590  resqrexlemover  10789  isumclim3  11199  algrp1  11733  tangtx  12935  coskpi  12945  subctctexmid  13249
  Copyright terms: Public domain W3C validator