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

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

Proof of Theorem syl5eq
StepHypRef Expression
1 syl5eq.1 . . 3 𝐴 = 𝐵
21a1i 9 . 2 (𝜑𝐴 = 𝐵)
3 syl5eq.2 . 2 (𝜑𝐵 = 𝐶)
42, 3eqtrd 2173 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  syl5req  2186  syl5eqr  2187  3eqtr3a  2197  3eqtr4g  2198  csbtt  3018  csbvarg  3034  csbie2g  3054  rabbi2dva  3288  csbprc  3412  disjssun  3430  disjpr2  3594  prprc2  3639  difprsn2  3667  opprc  3733  intsng  3812  riinm  3892  iinxsng  3893  iunxprg  3900  rintm  3912  sucprc  4341  unisucg  4343  xpriindim  4684  relop  4696  dmxpm  4766  riinint  4807  resabs1  4855  resabs2  4857  resima2  4860  xpssres  4861  resopab2  4873  imasng  4911  ndmima  4923  xpdisj1  4970  xpdisj2  4971  djudisj  4973  resdisj  4974  rnxpm  4975  xpima1  4992  xpima2m  4993  dmsnsnsng  5023  rnsnopg  5024  rnpropg  5025  mptiniseg  5040  dfco2a  5046  relcoi1  5077  unixpm  5081  iotaval  5106  funtp  5183  fnun  5236  fnresdisj  5240  fnima  5248  fnimaeq0  5251  fcoi1  5310  f1orescnv  5390  foun  5393  resdif  5396  tz6.12-2  5419  fveu  5420  tz6.12-1  5455  fvun2  5495  fvopab3ig  5502  f1oresrab  5592  dfmptg  5606  ressnop0  5608  fvunsng  5621  fnsnsplitss  5626  fsnunfv  5628  fvpr1  5631  fvpr2  5632  fvpr1g  5633  fvpr2g  5634  fvtp1g  5635  fvtp2g  5636  fvtp3g  5637  fvtp2  5639  fvtp3  5640  f1oiso2  5735  riotaund  5771  ovprc  5813  resoprab2  5875  fnoprabg  5879  ovidig  5895  ovigg  5898  ov6g  5915  ovconst2  5929  offval2  6004  ot1stg  6057  ot2ndg  6058  ot3rdgg  6059  fmpoco  6120  algrflemg  6134  tpostpos2  6169  rdgisuc1  6288  frec0g  6301  frecsuclem  6310  frecrdg  6312  oasuc  6367  oa1suc  6370  omsuc  6375  nnm1  6427  nnm2  6428  dfec2  6439  errn  6458  ixpsnval  6602  ixpintm  6626  mapen  6747  xpmapenlem  6750  phplem2  6754  undifdc  6819  fisseneq  6827  ssfirab  6829  eqinfti  6914  infvalti  6916  infsnti  6924  casef  6980  caseinl  6983  caseinr  6984  djudom  6985  ctssdccl  7003  exmidfodomrlemim  7073  1qec  7219  mulidnq  7220  addpinq1  7295  suplocexprlem2b  7545  suplocexprlemlub  7555  0idsr  7598  1idsr  7599  caucvgsrlemoffres  7631  caucvgsr  7633  mulresr  7669  pitonnlem2  7678  ax1rid  7708  axcnre  7712  negid  8032  subneg  8034  negneg  8035  dfinfre  8737  2times  8871  infrenegsupex  9415  rexneg  9642  xaddpnf2  9659  xaddmnf1  9660  xaddmnf2  9661  fseq1p1m1  9904  fzosplitprm1  10041  intfracq  10123  frec2uz0d  10202  frec2uzrdg  10212  frecuzrdg0  10216  frecuzrdgg  10219  frecuzrdg0t  10225  seq3val  10261  seqvalcd  10262  iseqf1olemjpcl  10298  iseqf1olemqpcl  10299  iseqf1olemfvp  10300  seq3f1olemqsum  10303  sqval  10381  iexpcyc  10427  binom3  10439  faclbnd  10518  faclbnd2  10519  bcn1  10535  hashinfom  10555  hashennn  10557  hashxp  10603  shftlem  10619  shftuz  10620  shftidt  10636  reim0  10664  remullem  10674  resqrexlemf1  10811  resqrexlemcalc3  10819  absexpzap  10883  absimle  10887  amgm2  10921  minmax  11032  xrmaxiflemval  11050  xrmaxadd  11061  infxrnegsupex  11063  xrminmax  11065  summodc  11183  fsum3  11187  sumsnf  11209  sumsns  11215  isumclim3  11223  isumge0  11230  fsump1i  11233  fsum2dlemstep  11234  fisumcom2  11238  fsumshftm  11245  fsumconst  11254  fsumiun  11277  hashrabrex  11281  hashuni  11282  binom11  11286  isumsplit  11291  geo2sum  11314  mertensabs  11337  prodmodc  11378  efgt1p2  11436  efgt1p  11437  resinval  11456  recosval  11457  cosadd  11478  ef01bndlem  11497  eirraplem  11517  ialgr0  11759  algrp1  11761  eucalg  11774  phiprmpw  11932  phiprm  11933  ennnfonelem0  11952  ennnfonelemfun  11964  ennnfonelemf1  11965  ennnfonelemrn  11966  ctinfomlemom  11974  ndxid  12020  setsfun0  12032  setsresg  12034  setscom  12036  strslfv2d  12038  ressid2  12055  ressval2  12056  tgidm  12280  tgrest  12375  ssidcn  12416  txcnmpt  12479  txcn  12481  blres  12640  mopnval  12648  remetdval  12745  divccncfap  12783  cncfmet  12785  cncfcncntop  12786  cnplimcim  12842  cnplimclemr  12844  limccnpcntop  12850  limccnp2cntop  12852  dvexp  12881  sin0pilem1  12908  pilem3  12910  ef2kpi  12933  sin2pim  12940  cos2pim  12941  sinmpi  12942  cosmpi  12943  sinppi  12944  cosppi  12945  sinhalfpip  12947  sinhalfpim  12948  coshalfpip  12949  coshalfpim  12950  tangtx  12965  1cxp  13027  ecxp  13028  rplogb1  13071  rpelogb  13072  ex-ceil  13107  qdencn  13395  cvgcmp2nlemabs  13400  trilpolemlt1  13407
  Copyright terms: Public domain W3C validator