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

Theorem 3eqtrd 2090
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 2086 . 2 (𝜑𝐵 = 𝐷)
51, 4eqtrd 2086 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047
This theorem is referenced by:  tpeq123d  3487  diftpsn3  3530  oteq123d  3589  resiima  4708  fvun1  5264  fvmptd  5278  fmptpr  5380  caovlem2d  5718  offval  5744  fnofval  5746  cnvf1olem  5870  nnm1  6125  ltexnqq  6534  prarloclemarch  6544  ltrnqg  6546  nq02m  6591  prarloclemcalc  6628  mulnqprl  6694  mulnqpru  6695  ltexprlemloc  6733  addcanprleml  6740  recexprlem1ssu  6760  cauappcvgprlem1  6785  caucvgsrlemfv  6903  caucvgsrlemoffval  6908  recidpirqlemcalc  6961  axmulass  6975  axrnegex  6981  muladd11r  7200  addcan2  7225  addsub  7255  subsub2  7272  negsubdi2  7303  muladd  7423  mulsub  7440  cru  7637  mulreim  7639  recextlem1  7676  mulap0  7679  muleqadd  7693  divrecap  7711  div23ap  7714  div12ap  7717  divcanap7  7742  conjmulap  7750  apmul1  7809  nndivtr  8001  xp1d2m1eqxm1d2  8204  div4p1lem1div2  8205  qapne  8641  xnegneg  8817  fseq1p1m1  9028  nn0split  9066  fzosplitsnm1  9137  fzosplitprm1  9162  ceilid  9230  flqdiv  9236  zmod10  9255  modqcyc  9274  modqaddabs  9277  mulqaddmodid  9279  modqadd2mod  9289  modqm1p1mod0  9290  modqmul12d  9293  modqadd12d  9295  modqmulmodr  9305  modqaddmulmod  9306  frecuzrdgsuc  9330  iseqid3s  9375  iseqid  9376  iseqhomo  9377  iseqz  9378  exp1  9391  expnegap0  9393  expmulzap  9431  m1expeven  9432  expdivap  9436  binom3  9498  sqoddm1div8  9533  bcn1  9590  bcnp1n  9591  ibcval5  9595  bcn2m1  9601  bcn2p1  9602  crim  9650  remullem  9663  remul2  9665  immul2  9672  ipcnval  9678  cjreim  9695  recvguniqlem  9784  resqrexlemover  9800  resqrexlemcalc1  9804  absid  9861  amgm2  9908  dvds2ln  10103  dvdseq  10123  opeo  10172
  Copyright terms: Public domain W3C validator