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

Theorem 3eqtrd 2121
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 2117 . 2 (𝜑𝐵 = 𝐷)
51, 4eqtrd 2117 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  tpeq123d  3517  diftpsn3  3561  oteq123d  3620  resiima  4757  fvun1  5333  fvmptd  5348  fmptpr  5452  caovlem2d  5794  offval  5820  fnofval  5822  cnvf1olem  5946  nnm1  6235  updjudhcoinlf  6715  updjudhcoinrg  6716  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  ltexnqq  6911  prarloclemarch  6921  ltrnqg  6923  nq02m  6968  prarloclemcalc  7005  mulnqprl  7071  mulnqpru  7072  ltexprlemloc  7110  addcanprleml  7117  recexprlem1ssu  7137  cauappcvgprlem1  7162  caucvgsrlemfv  7280  caucvgsrlemoffval  7285  recidpirqlemcalc  7338  axmulass  7352  axrnegex  7358  muladd11r  7582  addcan2  7607  addsub  7637  subsub2  7654  negsubdi2  7685  muladd  7806  mulsub  7823  cru  8020  mulreim  8022  recextlem1  8059  mulap0  8062  muleqadd  8076  divrecap  8094  div23ap  8097  div12ap  8100  divmulasscomap  8102  divcanap7  8127  conjmulap  8135  apmul1  8194  nndivtr  8398  xp1d2m1eqxm1d2  8601  div4p1lem1div2  8602  qapne  9056  xnegneg  9227  fseq1p1m1  9438  nn0split  9475  nnsplit  9476  fzosplitsnm1  9548  fzosplitprm1  9573  ceilid  9650  flqdiv  9656  zmod10  9675  modqcyc  9694  modqaddabs  9697  mulqaddmodid  9699  modqadd2mod  9709  modqm1p1mod0  9710  modqmul12d  9713  modqadd12d  9715  modqmulmodr  9725  modqaddmulmod  9726  frecuzrdgsuc  9749  iseqf1olemqsumkj  9832  iseqf1oleml  9837  iseqid3s  9842  iseqid  9843  iseqhomo  9845  iseqz  9846  exp1  9860  expnegap0  9862  expmulzap  9900  m1expeven  9901  expdivap  9905  binom3  9968  sqoddm1div8  10003  bcn1  10063  bcnp1n  10064  ibcval5  10068  bcn2m1  10074  bcn2p1  10075  hashdifpr  10125  crim  10188  remullem  10201  remul2  10203  immul2  10210  ipcnval  10216  cjreim  10233  recvguniqlem  10323  resqrexlemover  10339  resqrexlemcalc1  10343  absid  10400  amgm2  10447  max0addsup  10548  dvds2ln  10711  dvdseq  10731  opeo  10779  bezoutlemnewy  10867  eucalginv  10920  eucalglt  10921  eucialg  10923  lcmgcdlem  10941  lcm1  10945  divgcdcoprmex  10966  2sqpwodd  11036  zgcdsq  11061  qden1elz  11065  phiprmpw  11080  hashgcdlem  11085  peano4nninf  11341
  Copyright terms: Public domain W3C validator