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

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

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2143 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2184 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:  3eqtr3g  2195  csbeq1a  3012  ssdifeq0  3445  pofun  4234  opabbi2dv  4688  funimaexg  5207  fresin  5301  f1imacnv  5384  foimacnv  5385  fsn2  5594  fmptpr  5612  funiunfvdm  5664  funiunfvdmf  5665  fcof1o  5690  f1opw2  5976  fnexALT  6011  eqerlem  6460  pmresg  6570  mapsn  6584  fopwdom  6730  mapen  6740  fiintim  6817  xpfi  6818  sbthlemi8  6852  sbthlemi9  6853  ctssdccl  6996  exmidfodomrlemim  7062  mul02  8161  recdivap  8490  fzpreddisj  9863  fzshftral  9900  qbtwnrelemcalc  10045  frec2uzrdg  10194  frecuzrdgrcl  10195  frecuzrdgsuc  10199  frecuzrdgrclt  10200  frecuzrdgg  10201  binom3  10421  bcn2  10522  hashfz1  10541  hashunlem  10562  hashfacen  10591  cnrecnv  10694  resqrexlemnm  10802  amgm2  10902  2zsupmax  11009  xrmaxltsup  11039  xrmaxadd  11042  xrbdtri  11057  fisumss  11173  fsumcnv  11218  telfsumo  11247  fsumiun  11258  arisum2  11280  ege2le3  11389  efgt1p  11414  cos01bnd  11476  dfgcd3  11709  eucalgval  11746  sqrt2irrlem  11850  setsslid  12023  baspartn  12231  txdis1cn  12461  cnmpt21  12474  cnmpt22  12477  hmeores  12498  metreslem  12563  remetdval  12722  dvfvalap  12833  nninfsellemqall  13297
  Copyright terms: Public domain W3C validator