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

Theorem 3eqtr3d 2216
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2210 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2210 1 (𝜑𝐶 = 𝐷)
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:  mpteqb  5598  fvmptt  5599  fsnunfv  5709  f1ocnvfv1  5768  f1ocnvfv2  5769  fcof1  5774  caov12d  6046  caov13d  6048  caov411d  6050  caovimo  6058  tfrlem5  6305  tfrlemiubacc  6321  tfr1onlemubacc  6337  tfrcllemubacc  6350  nndir  6481  fopwdom  6826  updjud  7071  omp1eomlem  7083  addassnqg  7356  distrnqg  7361  enq0tr  7408  distrnq0  7433  distnq0r  7437  addnqprl  7503  addnqpru  7504  appdivnq  7537  ltmprr  7616  addcmpblnr  7713  mulcmpblnrlemg  7714  ltsrprg  7721  1idsr  7742  pn0sr  7745  mulgt0sr  7752  map2psrprg  7779  axmulass  7847  ax0id  7852  recriota  7864  mul12  8060  mul4  8063  readdcan  8071  add12  8089  cnegexlem2  8107  addcan  8111  ppncan  8173  addsub4  8174  subeqxfrd  8294  subaddeqd  8300  muladd  8315  mulcanapd  8591  receuap  8599  div13ap  8622  divdivdivap  8642  divcanap5  8643  divdivap1  8652  divdivap2  8653  halfaddsub  9124  fztp  10046  fseq1p1m1  10062  flqzadd  10266  flqdiv  10289  mulp1mod1  10333  modqnegd  10347  modqsub12d  10349  q2submod  10353  modsumfzodifsn  10364  seq3m1  10436  seq3caopr  10451  iseqf1olemab  10457  iseqf1olemnanb  10458  seq3f1olemqsumk  10467  exprecap  10529  expsubap  10536  zesq  10606  nn0opthlem1d  10666  facnn2  10680  faclbnd6  10690  zfz1isolemsplit  10785  seq3coll  10789  shftval3  10803  crre  10833  resub  10846  imsub  10854  cjsub  10868  bdtrilem  11214  bdtri  11215  climshft2  11281  nnf1o  11351  fsumf1o  11365  isumss  11366  fisumss  11367  fsumadd  11381  isumclim3  11398  fsummulc2  11423  fsumsub  11427  telfsumo  11441  telfsumo2  11442  hashiun  11453  bcxmas  11464  isumshft  11465  trireciplem  11475  geoserap  11482  geo2sum2  11490  fprodf1o  11563  prodssdc  11564  fprodssdc  11565  fprodmul  11566  fprodm1  11573  sinsub  11715  cossub  11716  p1modz1  11768  gcdaddm  11951  modgcd  11958  bezoutlemnewy  11963  absmulgcd  11984  gcdmultiplez  11988  eucalg  12025  lcmgcd  12044  lcmid  12046  numdensq  12168  dfphi2  12186  phiprm  12189  fermltl  12200  prmdiveq  12202  hashgcdlem  12204  odzdvds  12211  powm2modprm  12218  modprm0  12220  coprimeprodsq  12223  pythagtriplem6  12236  pythagtriplem7  12237  pythagtriplem12  12241  pythagtriplem14  12243  pythagtriplem16  12245  pcaddlem  12304  sumhashdc  12311  fldivp1  12312  pcfac  12314  pockthlem  12320  ennnfonelem1  12374  ennnfonelemex  12381  topnpropgd  12623  grprinvlem  12669  grprinvd  12670  grpridd  12671  mnd12g  12694  grprcan  12770  grplcan  12791  grpasscan1  12792  grpinv11  12798  grpinvnz  12800  grplmulf1o  12803  grpinvpropdg  12804  grpinvadd  12807  grpsubsub4  12822  dfgrp3m  12828  mhmid  12838  mhmmnd  12839  mulgz  12869  mulgdirlem  12872  mulgdir  12873  mulgass  12878  mulgsubdir  12881  restin  13169  blpnfctr  13432  xmssym  13462  limcimolemlt  13626  dvmulxxbr  13659  dvrecap  13670  dvmptaddx  13674  dvmptmulx  13675  dvmptnegcn  13677  dvmptsubcn  13678  dvmptcjx  13679  dveflem  13680  sin0pilem1  13695  ptolemy  13738  tangtx  13752  rpcxpneg  13821  rpcxpsub  13822  cxprec  13824  rpcxproot  13827  cxpcom  13850  rpabscxpbnd  13852  lgsvalmod  13913  lgsneg  13918  lgsdilem  13921  lgsne0  13932  lgssq  13934  lgssq2  13935  peano4nninf  14238  nninfalllem1  14240  nninfall  14241  nninfsellemqall  14247  qdencn  14258
  Copyright terms: Public domain W3C validator