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

Theorem 3eqtrd 2177
Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
Hypotheses
Ref Expression
3eqtrd.1 (𝜑𝐴 = 𝐵)
3eqtrd.2 (𝜑𝐵 = 𝐶)
3eqtrd.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
3eqtrd (𝜑𝐴 = 𝐷)

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2 (𝜑𝐴 = 𝐵)
2 3eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
3 3eqtrd.3 . . 3 (𝜑𝐶 = 𝐷)
42, 3eqtrd 2173 . 2 (𝜑𝐵 = 𝐷)
51, 4eqtrd 2173 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  tpeq123d  3622  diftpsn3  3668  oteq123d  3727  resiima  4904  fvun1  5494  fvmptd  5509  fmptpr  5619  caovlem2d  5970  offval  5996  ofvalg  5998  cnvf1olem  6128  nnm1  6427  updjudhcoinlf  6972  updjudhcoinrg  6973  caseinl  6983  caseinr  6984  omp1eomlem  6986  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  ltexnqq  7239  prarloclemarch  7249  ltrnqg  7251  nq02m  7296  prarloclemcalc  7333  mulnqprl  7399  mulnqpru  7400  ltexprlemloc  7438  addcanprleml  7445  recexprlem1ssu  7465  cauappcvgprlem1  7490  caucvgsrlemfv  7622  caucvgsrlemoffval  7627  recidpirqlemcalc  7688  axmulass  7704  axrnegex  7710  muladd11r  7941  addcan2  7966  addsub  7996  subsub2  8013  negsubdi2  8044  muladd  8169  mulsub  8186  cru  8387  mulreim  8389  recextlem1  8435  mulap0  8438  muleqadd  8452  divrecap  8471  div23ap  8474  div12ap  8477  divmulasscomap  8479  divcanap7  8504  conjmulap  8512  apmul1  8571  nndivtr  8785  xp1d2m1eqxm1d2  8995  div4p1lem1div2  8996  qapne  9457  xnegneg  9645  rexsub  9665  xnegid  9671  fseq1p1m1  9904  nn0split  9943  nnsplit  9944  fzosplitsnm1  10016  fzosplitprm1  10041  ceilid  10118  flqdiv  10124  zmod10  10143  modqcyc  10162  modqaddabs  10165  mulqaddmodid  10167  modqadd2mod  10177  modqm1p1mod0  10178  modqmul12d  10181  modqadd12d  10183  modqmulmodr  10193  modqaddmulmod  10194  frecuzrdgsuc  10217  seqeq123d  10257  seqvalcd  10262  seq3f1olemqsumkj  10301  seq3f1oleml  10306  seq3id3  10310  seq3id  10311  seq3homo  10313  seq3z  10314  exp1  10329  expnegap0  10331  expmulzap  10369  m1expeven  10370  expdivap  10374  binom3  10439  sqoddm1div8  10474  bcn1  10535  bcnp1n  10536  bcval5  10540  bcn2m1  10546  bcn2p1  10547  hashdifpr  10597  crim  10661  remullem  10674  remul2  10676  immul2  10683  ipcnval  10689  cjreim  10706  recvguniqlem  10797  resqrexlemover  10813  resqrexlemcalc1  10817  absid  10874  amgm2  10921  max0addsup  11022  minabs  11038  xrmaxrecl  11055  xrminadd  11075  fsumsplitf  11208  sumsnf  11209  fsump1i  11233  fsum2dlemstep  11234  fsumshftm  11245  fsummulc2  11248  modfsummodlemstep  11257  telfsumo  11266  fsumrelem  11271  hash2iun1dif1  11280  binomlem  11283  binom1dif  11287  arisum  11298  geo2sum  11314  geo2sum2  11315  cvgratz  11332  mertenslemi1  11335  clim2prod  11339  ef0lem  11401  eftlub  11431  efsep  11432  effsumlt  11433  tanval2ap  11454  efi4p  11458  resin4p  11459  recos4p  11460  efeul  11475  sinadd  11477  cosadd  11478  sinmul  11485  ef01bndlem  11497  cos12dec  11508  absef  11510  demoivreALT  11514  dvds2ln  11560  dvdseq  11580  opeo  11628  bezoutlemnewy  11718  eucalginv  11771  eucalglt  11772  eucalg  11774  lcmgcdlem  11792  lcm1  11796  divgcdcoprmex  11817  2sqpwodd  11888  zgcdsq  11913  qden1elz  11917  phiprmpw  11932  hashgcdlem  11937  xmetxpbl  12714  ivthinclemuopn  12822  limcimolemlt  12839  cnplimcim  12842  limccnpcntop  12850  limccnp2lem  12851  dvexp  12881  dvmptcmulcn  12889  ef2kpi  12933  sinhalfpip  12947  sinhalfpim  12948  coshalfpim  12950  ptolemy  12951  tangtx  12965  rpabscxpbnd  13065  relogbexpap  13081  rplogbcxp  13086  rpcxplogb  13087  peano4nninf  13373  trilpolemclim  13402  trilpolemeq1  13406  apdifflemf  13412
  Copyright terms: Public domain W3C validator