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

Theorem syl5eq 2129
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 2117 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  syl5req  2130  syl5eqr  2131  3eqtr3a  2141  3eqtr4g  2142  csbtt  2932  csbvarg  2947  csbie2g  2967  rabbi2dva  3197  csbprc  3316  disjssun  3334  disjpr2  3491  prprc2  3536  difprsn2  3562  opprc  3628  intsng  3707  riinm  3787  iinxsng  3788  rintm  3802  sucprc  4215  unisucg  4217  xpriindim  4544  relop  4556  dmxpm  4626  riinint  4664  resabs1  4711  resabs2  4712  resima2  4715  xpssres  4716  resopab2  4728  imasng  4766  ndmima  4778  xpdisj1  4823  xpdisj2  4824  djudisj  4826  resdisj  4827  rnxpm  4828  xpima1  4845  xpima2m  4846  dmsnsnsng  4876  rnsnopg  4877  rnpropg  4878  mptiniseg  4893  dfco2a  4899  relcoi1  4930  unixpm  4934  iotaval  4959  funtp  5034  fnun  5087  fnresdisj  5091  fnima  5099  fnimaeq0  5102  fcoi1  5156  f1orescnv  5234  foun  5237  resdif  5240  tz6.12-2  5261  fveu  5262  tz6.12-1  5296  fvun2  5336  fvopab3ig  5343  f1oresrab  5428  dfmptg  5441  ressnop0  5443  fvunsng  5456  fsnunfv  5462  fvpr1  5464  fvpr2  5465  fvpr1g  5466  fvpr2g  5467  fvtp1g  5468  fvtp2g  5469  fvtp3g  5470  fvtp2  5472  fvtp3  5473  f1oiso2  5569  riotaund  5605  ovprc  5643  resoprab2  5701  fnoprabg  5705  ovidig  5721  ovigg  5724  ov6g  5741  ovconst2  5755  offval2  5829  ot1stg  5882  ot2ndg  5883  ot3rdgg  5884  fmpt2co  5940  algrflemg  5954  tpostpos2  5986  rdgisuc1  6105  frec0g  6118  frecsuclem  6127  frecrdg  6129  oasuc  6181  oa1suc  6184  omsuc  6189  nnm1  6237  nnm2  6238  dfec2  6249  errn  6268  mapen  6516  xpmapenlem  6519  phplem2  6523  undifdc  6588  fisseneq  6595  ssfirab  6596  eqinfti  6662  infvalti  6664  infsnti  6672  casef  6726  djudom  6734  exmidfodomrlemim  6774  1qec  6894  mulidnq  6895  addpinq1  6970  0idsr  7260  1idsr  7261  caucvgsrlemoffres  7292  caucvgsr  7294  mulresr  7322  pitonnlem2  7331  ax1rid  7359  axcnre  7363  negid  7676  subneg  7678  negneg  7679  dfinfre  8355  2times  8481  infrenegsupex  9017  rexneg  9227  fseq1p1m1  9441  fzosplitprm1  9576  intfracq  9658  frec2uz0d  9737  frec2uzrdg  9747  frecuzrdg0  9751  frecuzrdgg  9754  frecuzrdg0t  9760  iseqval  9802  iseqvalt  9804  seq3-1  9807  iseqf1olemjpcl  9848  iseqf1olemqpcl  9849  iseqf1olemfvp  9850  iseqf1olemqsum  9853  sqval  9933  iexpcyc  9978  binom3  9989  faclbnd  10067  faclbnd2  10068  bcn1  10084  hashinfom  10104  hashennn  10106  hashxp  10152  shftlem  10168  shftuz  10169  shftidt  10185  reim0  10212  remullem  10222  resqrexlemf1  10358  resqrexlemcalc3  10366  absexpzap  10430  absimle  10434  amgm2  10468  minmax  10577  isummo  10686  fisum  10689  sumsnf  10710  sumsns  10715  ialgr0  10951  ialgrp1  10953  eucialg  10966  phiprmpw  11123  phiprm  11124  ex-ceil  11142  qdencn  11403
  Copyright terms: Public domain W3C validator