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

Theorem syl5eq 2084
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 2072 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:  syl5req  2085  syl5eqr  2086  3eqtr3a  2096  3eqtr4g  2097  csbtt  2862  csbvarg  2877  csbie2g  2896  rabbi2dva  3145  csbprc  3262  disjssun  3285  disjpr2  3434  prprc2  3479  difprsn2  3504  opprc  3570  intsng  3649  riinm  3729  iinxsng  3730  rintm  3744  sucprc  4149  unisucg  4151  xpriindim  4474  relop  4486  dmxpm  4555  riinint  4593  resabs1  4640  resabs2  4641  resima2  4644  xpssres  4645  resopab2  4655  imasng  4690  ndmima  4702  xpdisj1  4747  xpdisj2  4748  djudisj  4750  resdisj  4751  rnxpm  4752  xpima1  4767  xpima2m  4768  dmsnsnsng  4798  rnsnopg  4799  rnpropg  4800  mptiniseg  4815  dfco2a  4821  relcoi1  4849  unixpm  4853  iotaval  4878  funtp  4952  fnun  5005  fnresdisj  5009  fnima  5017  fnimaeq0  5020  fcoi1  5070  f1orescnv  5142  foun  5145  resdif  5148  tz6.12-2  5169  fveu  5170  tz6.12-1  5200  fvun2  5240  fvopab3ig  5246  f1oresrab  5329  dfmptg  5342  ressnop0  5344  fvunsng  5357  fsnunfv  5363  fvpr1  5365  fvpr2  5366  fvpr1g  5367  fvpr2g  5368  fvtp1g  5369  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  f1oiso2  5466  riotaund  5502  ovprc  5540  resoprab2  5598  fnoprabg  5602  ovidig  5618  ovigg  5621  ov6g  5638  ovconst2  5652  offval2  5726  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  fmpt2co  5837  algrflemg  5851  tpostpos2  5880  rdgisuc1  5971  frec0g  5983  frecsuclem1  5987  frecsuclem2  5989  frecrdg  5992  oasuc  6044  oa1suc  6047  omsuc  6051  nnm1  6097  nnm2  6098  dfec2  6109  errn  6128  phplem2  6316  1qec  6484  mulidnq  6485  addpinq1  6560  0idsr  6850  1idsr  6851  caucvgsrlemoffres  6882  caucvgsr  6884  mulresr  6912  pitonnlem2  6921  ax1rid  6949  axcnre  6953  negid  7256  subneg  7258  negneg  7259  2times  8036  rexneg  8741  fseq1p1m1  8954  fzosplitprm1  9088  frec2uz0d  9159  frec2uzrdg  9169  frecuzrdg0  9174  iseqval  9194  sqval  9286  binom3  9340  shftlem  9391  shftuz  9392  shftidt  9408  reim0  9435  remullem  9445  resqrexlemf1  9580  resqrexlemcalc3  9588  absexpzap  9650  absimle  9654  amgm2  9688  ialgr0  9857  ialgrp1  9859  ex-ceil  9870  qdencn  10097
  Copyright terms: Public domain W3C validator