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

Theorem 3eqtrd 2118
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 2114 . 2 (𝜑𝐵 = 𝐷)
51, 4eqtrd 2114 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  tpeq123d  3486  diftpsn3  3529  oteq123d  3587  resiima  4707  fvun1  5265  fvmptd  5279  fmptpr  5381  caovlem2d  5718  offval  5744  fnofval  5746  cnvf1olem  5870  nnm1  6156  ltexnqq  6649  prarloclemarch  6659  ltrnqg  6661  nq02m  6706  prarloclemcalc  6743  mulnqprl  6809  mulnqpru  6810  ltexprlemloc  6848  addcanprleml  6855  recexprlem1ssu  6875  cauappcvgprlem1  6900  caucvgsrlemfv  7018  caucvgsrlemoffval  7023  recidpirqlemcalc  7076  axmulass  7090  axrnegex  7096  muladd11r  7320  addcan2  7345  addsub  7375  subsub2  7392  negsubdi2  7423  muladd  7544  mulsub  7561  cru  7758  mulreim  7760  recextlem1  7797  mulap0  7800  muleqadd  7814  divrecap  7832  div23ap  7835  div12ap  7838  divmulasscomap  7840  divcanap7  7865  conjmulap  7873  apmul1  7932  nndivtr  8136  xp1d2m1eqxm1d2  8339  div4p1lem1div2  8340  qapne  8794  xnegneg  8965  fseq1p1m1  9176  nn0split  9213  fzosplitsnm1  9284  fzosplitprm1  9309  ceilid  9386  flqdiv  9392  zmod10  9411  modqcyc  9430  modqaddabs  9433  mulqaddmodid  9435  modqadd2mod  9445  modqm1p1mod0  9446  modqmul12d  9449  modqadd12d  9451  modqmulmodr  9461  modqaddmulmod  9462  frecuzrdgsuc  9485  iseqid3s  9551  iseqid  9552  iseqhomo  9554  iseqz  9555  exp1  9568  expnegap0  9570  expmulzap  9608  m1expeven  9609  expdivap  9613  binom3  9676  sqoddm1div8  9711  bcn1  9771  bcnp1n  9772  ibcval5  9776  bcn2m1  9782  bcn2p1  9783  crim  9872  remullem  9885  remul2  9887  immul2  9894  ipcnval  9900  cjreim  9917  recvguniqlem  10007  resqrexlemover  10023  resqrexlemcalc1  10027  absid  10084  amgm2  10131  max0addsup  10232  dvds2ln  10362  dvdseq  10382  opeo  10430  bezoutlemnewy  10518  eucalginv  10571  eucalglt  10572  eucialg  10574  lcmgcdlem  10592  lcm1  10596  divgcdcoprmex  10617  2sqpwodd  10687
  Copyright terms: Public domain W3C validator