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

Theorem syl5eq 2062
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eq.1 A = B
syl5eq.2 (φB = 𝐶)
Assertion
Ref Expression
syl5eq (φA = 𝐶)

Proof of Theorem syl5eq
StepHypRef Expression
1 syl5eq.1 . . 3 A = B
21a1i 9 . 2 (φA = B)
3 syl5eq.2 . 2 (φB = 𝐶)
42, 3eqtrd 2050 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1226
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 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  syl5req  2063  syl5eqr  2064  3eqtr3a  2074  3eqtr4g  2075  csbtt  2835  csbvarg  2850  csbie2g  2869  rabbi2dva  3118  csbprc  3235  disjssun  3258  disjpr2  3404  prprc2  3449  difprsn2  3474  opprc  3540  intsng  3619  riinm  3699  iinxsng  3700  rintm  3714  sucprc  4094  unisucg  4096  xpriindim  4397  relop  4409  dmxpm  4478  riinint  4516  resabs1  4563  resabs2  4564  resima2  4567  xpssres  4568  resopab2  4578  imasng  4613  ndmima  4625  xpdisj1  4670  xpdisj2  4671  djudisj  4673  resdisj  4674  rnxpm  4675  xpima1  4690  xpima2m  4691  dmsnsnsng  4721  rnsnopg  4722  rnpropg  4723  mptiniseg  4738  dfco2a  4744  relcoi1  4772  unixpm  4776  iotaval  4801  funtp  4874  fnun  4927  fnresdisj  4931  fnima  4939  fnimaeq0  4942  fcoi1  4991  f1orescnv  5063  foun  5066  resdif  5069  tz6.12-2  5090  fveu  5091  tz6.12-1  5121  fvun2  5161  fvopab3ig  5167  f1oresrab  5250  dfmptg  5263  ressnop0  5265  fvunsng  5278  fsnunfv  5284  fvpr1  5286  fvpr2  5287  fvpr1g  5288  fvpr2g  5289  fvtp1g  5290  fvtp2g  5291  fvtp3g  5292  fvtp2  5294  fvtp3  5295  f1oiso2  5387  riotaund  5422  ovprc  5459  resoprab2  5517  fnoprabg  5521  ovidig  5537  ovigg  5540  ov6g  5557  ovconst2  5571  offval2  5645  ot1stg  5698  ot2ndg  5699  ot3rdgg  5700  fmpt2co  5756  tpostpos2  5798  rdgisuc1  5887  frec0g  5898  frecsuclem1  5899  frecsuclem2  5901  frecrdg  5904  oasuc  5955  oa1suc  5958  omsuc  5962  nnm1  6004  nnm2  6005  dfec2  6016  errn  6035  1qec  6241  mulidnq  6242  0idsr  6508  1idsr  6509  mulresr  6543  ax1rid  6565  axcnre  6569  negid  6844  subneg  6846  negneg  6847
  Copyright terms: Public domain W3C validator