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

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

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
2 3eqtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
3 3eqtr4d.1 . . 3 (𝜑𝐴 = 𝐵)
42, 3eqtr4d 2075 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2075 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  fnsnfv  5232  fvco2  5242  resfunexg  5382  fcof1  5423  fliftfun  5436  caovdir2d  5677  caov32d  5681  caov31d  5683  caov4d  5685  caovlem2d  5693  caofcom  5734  cnvf1olem  5845  tfrlem1  5923  tfrlemisucaccv  5939  frecrdg  5992  oav2  6043  omv2  6045  omsuc  6051  nnmsucr  6067  ecovicom  6214  ecoviass  6216  ecovidi  6218  carden2bex  6367  addcompig  6425  addasspig  6426  mulcompig  6427  mulasspig  6428  distrpig  6429  addassnqg  6478  addnq0mo  6543  mulnq0mo  6544  nqnq0a  6550  nqnq0m  6551  distrnq0  6555  mulcomnq0  6556  addassnq0  6558  addcmpblnr  6822  mulcmpblnrlemg  6823  addsrmo  6826  mulsrmo  6827  ltsrprg  6830  recexgt0sr  6856  mulgt0sr  6860  mulextsr1lem  6862  addcnsrec  6916  mulcnsrec  6917  pitonnlem2  6921  recidpirqlemcalc  6931  axaddcom  6942  adddir  7016  mul32  7141  mul31  7142  add32  7168  add4  7170  sub32  7243  sub4  7254  subdir  7381  mulneg2  7391  mulreim  7593  apadd1  7597  apneg  7600  divassap  7667  divdirap  7672  divmul13ap  7689  divmul24ap  7690  divdiv32ap  7694  conjmulap  7703  zeo  8341  lincmb01cmp  8869  iccf1o  8870  flhalf  9142  iseqshft2  9206  iseqcaopr3  9214  iseqcaopr  9216  iseqhomo  9222  iseqdistr  9223  expp1  9236  expnegap0  9237  expaddzaplem  9272  expaddzap  9273  expmulzap  9275  sqneg  9287  sqdivap  9292  subsq2  9333  binom2  9336  shftfibg  9395  shftfib  9398  shftval  9400  2shfti  9406  crre  9431  remim  9434  mulreap  9438  reneg  9442  readd  9443  remullem  9445  redivap  9448  imneg  9450  imadd  9451  imdivap  9455  cjcj  9457  cjadd  9458  cjmulrcl  9461  cjneg  9464  imval2  9468  resqrexlemcalc1  9586  absneg  9622  sqabsadd  9627  sqabssub  9628  absmul  9641  absresq  9648  absexp  9649  absexpzap  9650  serif0  9845
  Copyright terms: Public domain W3C validator