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

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

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2119 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2119 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:  mpteqb  5356  fvmptt  5357  fsnunfv  5460  f1ocnvfv1  5517  f1ocnvfv2  5518  fcof1  5523  caov12d  5783  caov13d  5785  caov411d  5787  caovimo  5795  grprinvlem  5796  grprinvd  5797  grpridd  5798  tfrlem5  6033  tfrlemiubacc  6049  tfr1onlemubacc  6065  tfrcllemubacc  6078  nndir  6205  fopwdom  6504  updjud  6717  addassnqg  6885  distrnqg  6890  enq0tr  6937  distrnq0  6962  distnq0r  6966  addnqprl  7032  addnqpru  7033  appdivnq  7066  ltmprr  7145  addcmpblnr  7229  mulcmpblnrlemg  7230  ltsrprg  7237  1idsr  7258  pn0sr  7261  mulgt0sr  7267  axmulass  7352  ax0id  7357  recriota  7369  mul12  7555  mul4  7558  readdcan  7566  add12  7584  cnegexlem2  7602  addcan  7606  ppncan  7668  addsub4  7669  subaddeqd  7791  muladd  7806  mulcanapd  8069  receuap  8077  div13ap  8099  divdivdivap  8119  divcanap5  8120  divdivap1  8129  divdivap2  8130  halfaddsub  8583  fztp  9422  fseq1p1m1  9438  flqzadd  9633  flqdiv  9656  mulp1mod1  9700  modqnegd  9714  modqsub12d  9716  q2submod  9720  modsumfzodifsn  9731  iseqm1  9801  iseqcaopr  9816  iseqf1olemab  9822  iseqf1olemnanb  9823  iseqf1olemqsumk  9832  exprecap  9894  expsubap  9901  zesq  9968  nn0opthlem1d  10024  facnn2  10038  faclbnd6  10048  zfz1isolemsplit  10139  iseqcoll  10143  shftval3  10157  crre  10186  resub  10199  imsub  10207  cjsub  10221  climshft2  10587  isummolemnm  10658  fsumf1o  10668  isumss  10669  fisumss  10670  gcdaddm  10850  modgcd  10857  bezoutlemnewy  10860  absmulgcd  10881  gcdmultiplez  10885  eucialg  10916  lcmgcd  10935  lcmid  10937  numdensq  11055  dfphi2  11071  phiprm  11074  hashgcdlem  11078  peano4nninf  11334  nninfalllem1  11337  nninfall  11338  nninfsellemqall  11345  qdencn  11353
  Copyright terms: Public domain W3C validator