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

Theorem eqtrdi 2224
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrdi.1  |-  ( ph  ->  A  =  B )
eqtrdi.2  |-  B  =  C
Assertion
Ref Expression
eqtrdi  |-  ( ph  ->  A  =  C )

Proof of Theorem eqtrdi
StepHypRef Expression
1 eqtrdi.1 . 2  |-  ( ph  ->  A  =  B )
2 eqtrdi.2 . . 3  |-  B  =  C
32a1i 9 . 2  |-  ( ph  ->  B  =  C )
41, 3eqtrd 2208 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157
This theorem depends on definitions:  df-bi 117  df-cleq 2168
This theorem is referenced by:  eqtr2di  2225  eqtr4di  2226  3eqtr3g  2231  3eqtr4a  2234  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  cbvrabcsf  3120  csbprc  3466  un00  3467  disjssun  3484  disjpr2  3653  tppreq3  3692  diftpsn3  3730  preq12b  3766  intsng  3874  uniintsnr  3876  rint0  3879  riin0  3953  iununir  3965  intexr  4145  sucprc  4406  op1stbg  4473  elreldm  4846  xpeq0r  5043  xpdisj1  5045  xpdisj2  5046  resdisj  5049  xpima1  5067  xpima2m  5068  elxp4  5108  unixp0im  5157  uniabio  5180  iotass  5187  cnvresid  5282  funimacnv  5284  f1o00  5488  dffv4g  5504  fnrnfv  5554  feqresmpt  5562  dffn5imf  5563  funfvdm2f  5573  fvun1  5574  fvmpt2  5591  fndmin  5615  fmptcof  5675  fmptcos  5676  fvunsng  5702  fvpr1  5712  fnrnov  6010  offval  6080  ofrfval  6081  op1std  6139  op2ndd  6140  fmpoco  6207  tpostpos  6255  tfr0  6314  rdgival  6373  frec0g  6388  2oconcl  6430  om0  6449  oei0  6450  oasuc  6455  omv2  6456  nnm0r  6470  uniqs2  6585  en1  6789  en1bg  6790  fundmen  6796  mapsnen  6801  xpsnen  6811  xpcomco  6816  xpdom2  6821  xpmapenlem  6839  exmidpweq  6899  unsnfidcex  6909  fiintim  6918  ssfirab  6923  sbthlemi8  6953  elfi2  6961  fi0  6964  fieq0  6965  djudom  7082  ismkvnex  7143  nninfwlpoimlemg  7163  en2other2  7185  exmidfodomrlemim  7190  nq0m0r  7430  addpinq1  7438  genipv  7483  genpelvl  7486  genpelvu  7487  cauappcvgprlem1  7633  caucvgsrlemoffres  7774  addresr  7811  mulresr  7812  axcnre  7855  add20  8405  rimul  8516  rereim  8517  mulreim  8535  sup3exmid  8885  fv0p1e1  9005  div4p1lem1div2  9143  nnm1nn0  9188  znegcl  9255  peano2z  9260  nneoor  9326  nn0ind-raph  9341  xnegneg  9802  xltnegi  9804  xaddpnf1  9815  xnegid  9828  xnn0xadd0  9836  xnegdi  9837  xsubge0  9850  xposdif  9851  xlesubadd  9852  xleaddadd  9856  fz0to4untppr  10092  fzo0to2pr  10186  fldiv4p1lem1div2  10273  mulp1mod1  10333  frecfzennn  10394  iseqf1olemqk  10462  exp0  10492  expp1  10495  expnegap0  10496  1exp  10517  mulexp  10527  m1expeven  10535  sq0i  10579  bernneq  10608  facp1  10676  faclbnd3  10689  facubnd  10691  bcval5  10709  hashinfom  10724  hashsng  10745  hashxp  10773  resunimafz0  10778  zfz1iso  10788  imre  10827  reim0b  10838  rereb  10839  resqrexlemover  10986  resqrexlemcalc1  10990  abs00bd  11042  maxabslemlub  11183  xrmaxiflemcom  11224  xrmaxadd  11236  climconst  11265  isumz  11364  fsumf1o  11365  fsumcllem  11374  fsumadd  11381  fsumxp  11411  fsumcnv  11412  fsummulc2  11423  fsumconst  11429  fsumabs  11440  telfsumo  11441  fsumparts  11445  fsumrelem  11446  fsumiun  11452  binomlem  11458  binom  11459  binom11  11461  isumsplit  11466  arisum  11473  arisum2  11474  trireciplem  11475  georeclim  11488  cvgratnnlemseq  11501  prodfrecap  11521  prod1dc  11561  fprodf1o  11563  fprodcl2lem  11580  fprodcllem  11581  fprodfac  11590  fprod2d  11598  fprodxp  11599  fprodcnv  11600  fprodrec  11604  fprodmodd  11616  ef0lem  11635  ege2le3  11646  efaddlem  11649  efcan  11651  eft0val  11668  ef4p  11669  efgt1p2  11670  efi4p  11692  sincossq  11723  cos2tsin  11726  absefi  11743  demoivreALT  11748  p1modz1  11768  dvdsabseq  11819  odd2np1lem  11843  oddp1even  11847  opoe  11866  m1expo  11871  m1exp1  11872  nn0o1gt2  11876  nninfdcex  11920  gcddvds  11930  gcdcl  11933  gcdeq0  11944  gcd0id  11946  bezoutr1  12000  nnmindc  12001  nnminle  12002  eucalg  12025  lcm0val  12031  lcmid  12046  rpmul  12064  dfphi2  12186  phiprmpw  12188  hashgcdeq  12205  odzdvds  12211  nnnn0modprm0  12221  pythagtriplem4  12234  pythagtriplem12  12241  pcaddlem  12304  pcmpt  12307  pockthi  12322  ennnfonelem0  12372  ennnfonelem1  12374  ennnfonelemhdmp1  12376  ennnfonelemkh  12379  ennnfonelemhf1o  12380  ennnfonelemf1  12385  ctiunctlemfo  12406  setsresg  12466  strle1g  12520  restid2  12618  grplactcnv  12831  mulg0  12847  mulgneg  12860  mulgneg2  12875  tgval2  13044  tgidm  13067  epttop  13083  tgrest  13162  restco  13167  restsn  13173  tgcn  13201  cnptopresti  13231  cnptoprest  13232  txbas  13251  upxp  13265  txrest  13269  txdis  13270  txhmeo  13312  txswaphmeolem  13313  xblss2ps  13397  xblss2  13398  qtopbasss  13514  fsumcncntop  13549  limcimolemlt  13626  dvcnp2cntop  13656  dvcoapbr  13664  dvexp  13668  dvexp2  13669  dveflem  13680  dvef  13681  sin0pilem1  13695  sin2kpi  13725  cos2kpi  13726  coseq0q4123  13748  coseq0negpitopi  13750  sincosq1eq  13753  sinkpi  13761  coskpi  13762  1cxp  13814  lgslem2  13895  lgsfcl2  13900  lgs0  13907  lgs2  13911  lgsneg  13918  lgsdilem  13921  lgsdir2lem4  13925  lgsdir2lem5  13926  lgsne0  13932  lgssq  13934  lgssq2  13935  2sqlem9  13953  2sqlem10  13954  ex-ceil  13960  bj-intexr  14142  exmid1stab  14232  peano3nninf  14239  nninfall  14241  isomninnlem  14261  iswomni0  14282  ismkvnnlem  14283  nconstwlpolem0  14293
  Copyright terms: Public domain W3C validator