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

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

Proof of Theorem syl6eq
StepHypRef Expression
1 syl6eq.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eq.2 . . 3 𝐵 = 𝐶
32a1i 9 . 2 (𝜑𝐵 = 𝐶)
41, 3eqtrd 2120 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  syl6req  2137  syl6eqr  2138  3eqtr3g  2143  3eqtr4a  2146  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  csbprc  3325  un00  3326  disjssun  3343  disjpr2  3501  tppreq3  3540  diftpsn3  3573  preq12b  3609  intsng  3717  uniintsnr  3719  rint0  3722  riin0  3796  iununir  3807  intexr  3978  sucprc  4230  op1stbg  4291  elreldm  4649  xpeq0r  4841  xpdisj1  4842  xpdisj2  4843  resdisj  4846  xpima1  4864  xpima2m  4865  elxp4  4905  unixp0im  4954  uniabio  4977  iotass  4984  cnvresid  5074  funimacnv  5076  f1o00  5272  dffv4g  5286  fnrnfv  5335  feqresmpt  5342  dffn5imf  5343  funfvdm2f  5353  fvun1  5354  fvmpt2  5370  fndmin  5390  fmptcof  5449  fmptcos  5450  fvunsng  5475  fvpr1  5483  fnrnov  5772  offval  5845  ofrfval  5846  op1std  5901  op2ndd  5902  fmpt2co  5963  tpostpos  6011  tfr0  6070  rdgival  6129  frec0g  6144  2oconcl  6185  om0  6201  oei0  6202  oasuc  6207  omv2  6208  nnm0r  6222  uniqs2  6332  en1  6496  en1bg  6497  fundmen  6503  mapsnen  6508  xpsnen  6517  xpcomco  6522  xpdom2  6527  xpmapenlem  6545  unsnfidcex  6610  ssfirab  6622  sbthlemi8  6652  djudom  6766  en2other2  6801  exmidfodomrlemim  6806  nq0m0r  6994  addpinq1  7002  genipv  7047  genpelvl  7050  genpelvu  7051  cauappcvgprlem1  7197  caucvgsrlemoffres  7324  addresr  7353  mulresr  7354  axcnre  7395  add20  7931  rimul  8038  rereim  8039  mulreim  8057  div4p1lem1div2  8639  nnm1nn0  8684  znegcl  8751  peano2z  8756  nneoor  8818  nn0ind-raph  8833  xnegneg  9264  xltnegi  9266  fzo0to2pr  9594  fldiv4p1lem1div2  9677  mulp1mod1  9737  frecfzennn  9798  iseqf1olemqk  9888  exp0  9924  expp1  9927  expnegap0  9928  1exp  9949  mulexp  9959  m1expeven  9967  sq0i  10011  bernneq  10039  facp1  10103  faclbnd3  10116  facubnd  10118  ibcval5  10136  hashinfom  10151  hashsng  10171  hashxp  10199  resunimafz0  10201  zfz1iso  10211  imre  10250  reim0b  10261  rereb  10262  resqrexlemover  10408  resqrexlemcalc1  10412  abs00bd  10464  maxabslemlub  10605  climconst  10642  isumz  10745  fsumf1o  10746  fsumcllem  10756  fsumadd  10763  fsumxp  10793  fsumcnv  10794  fsummulc2  10805  fsumconst  10811  fsumabs  10822  telfsumo  10823  fsumparts  10827  fsumrelem  10828  fsumiun  10833  binomlem  10839  binom  10840  binom11  10842  isumsplit  10847  arisum  10853  arisum2  10854  trireciplem  10855  georeclim  10868  cvgratnnlemseq  10881  dvdsabseq  10941  odd2np1lem  10965  oddp1even  10969  opoe  10988  m1expo  10993  m1exp1  10994  nn0o1gt2  10998  gcddvds  11048  gcdcl  11051  gcdeq0  11061  gcd0id  11063  bezoutr1  11115  eucialg  11134  lcm0val  11140  lcmid  11155  rpmul  11173  dfphi2  11289  phiprmpw  11291  hashgcdeq  11297  ex-ceil  11310  bj-intexr  11456  peano3nninf  11554  nninfall  11557
  Copyright terms: Public domain W3C validator