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

Theorem 3eqtr4d 2127
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 2120 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2120 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:  fnsnfv  5328  fvco2  5338  resfunexg  5481  fcof1  5525  fliftfun  5538  caovdir2d  5780  caov32d  5784  caov31d  5786  caov4d  5788  caovlem2d  5796  caofcom  5837  cnvf1olem  5948  tfrlem1  6029  tfrlemisucaccv  6046  tfr1onlemsucaccv  6062  tfrcllemsucaccv  6075  frecrdg  6129  oav2  6180  omv2  6182  omsuc  6189  nnmsucr  6205  ecovicom  6354  ecoviass  6356  ecovidi  6358  carden2bex  6764  addcompig  6835  addasspig  6836  mulcompig  6837  mulasspig  6838  distrpig  6839  addassnqg  6888  addnq0mo  6953  mulnq0mo  6954  nqnq0a  6960  nqnq0m  6961  distrnq0  6965  mulcomnq0  6966  addassnq0  6968  addcmpblnr  7232  mulcmpblnrlemg  7233  addsrmo  7236  mulsrmo  7237  ltsrprg  7240  recexgt0sr  7266  mulgt0sr  7270  mulextsr1lem  7272  addcnsrec  7326  mulcnsrec  7327  pitonnlem2  7331  recidpirqlemcalc  7341  axaddcom  7352  adddir  7426  mul32  7559  mul31  7560  add32  7588  add4  7590  sub32  7663  sub4  7674  subdir  7811  mulneg2  7821  mulreim  8025  apadd1  8029  apneg  8032  divassap  8099  divdirap  8106  divmul13ap  8124  divmul24ap  8125  divdiv32ap  8129  conjmulap  8138  zeo  8787  lincmb01cmp  9355  iccf1o  9356  flhalf  9640  modqvalp1  9681  modqdi  9730  modqsubdir  9731  frecuzrdgg  9754  iseqshft2  9810  iseqcaopr3  9818  iseqcaopr  9820  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  iseqf1olemqsum  9837  iseqhomo  9848  iseqdistr  9850  expp1  9864  expnegap0  9865  expaddzaplem  9900  expaddzap  9901  expmulzap  9903  sqneg  9916  sqdivap  9921  subsq2  9963  binom2  9966  facp1  10038  bcm1k  10068  bcp1n  10069  ibcval5  10071  omgadd  10110  hashun  10113  hashxp  10134  shftfibg  10154  shftfib  10157  shftval  10159  2shfti  10165  crre  10190  remim  10193  mulreap  10197  reneg  10201  readd  10202  remullem  10204  redivap  10207  imneg  10209  imadd  10210  imdivap  10214  cjcj  10216  cjadd  10217  cjmulrcl  10220  cjneg  10223  imval2  10227  resqrexlemcalc1  10346  absneg  10382  sqabsadd  10387  sqabssub  10388  absmul  10401  absresq  10410  absexp  10411  absexpzap  10412  serif0  10636  isummolem3  10664  fisum  10670  isumss  10674  fisumss  10675  fsumadd  10688  odd2np1lem  10778  oexpneg  10783  neggcd  10880  gcdabs2  10887  mulgcd  10911  mulgcdr  10913  gcddiv  10914  rplpwr  10922  eucalgval  10942  eucalginv  10944  eucialg  10947  neglcm  10963  lcmgcd  10966  mulgcddvds  10982  qredeu  10985  nn0gcdsq  11084  phimullem  11107  nninfalllemn  11367  nninfsellemeqinf  11377
  Copyright terms: Public domain W3C validator