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

Theorem eqtr4d 2075
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr4d.1 (𝜑𝐴 = 𝐵)
eqtr4d.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
eqtr4d (𝜑𝐴 = 𝐶)

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqtr4d.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2045 . 2 (𝜑𝐵 = 𝐶)
41, 3eqtrd 2072 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:  3eqtr2d  2078  3eqtr2rd  2079  3eqtr4d  2082  3eqtr4rd  2083  3eqtr4a  2098  sbnfc2  2906  onsucuni2  4288  relop  4486  riinint  4593  iotauni  4879  fniinfv  5231  fsn2  5337  fmptapd  5354  fconst2g  5376  fniunfv  5401  ofres  5725  ofco  5729  frecsuclem2  5989  frecrdg  5992  oasuc  6044  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  uniqs2  6166  en1bg  6280  fundmen  6286  phplem4dom  6324  addcmpblnq  6463  distrnqg  6483  ltexnqq  6504  addcmpblnq0  6539  nqnq0a  6550  nqnq0m  6551  nq0m0r  6552  nq0a0  6553  nnanq0  6554  distrnq0  6555  prarloclemlo  6590  prarloclemcalc  6598  genpassl  6620  genpassu  6621  ltsosr  6847  0idsr  6850  1idsr  6851  mulextsr1lem  6862  cnegex  7187  subsub3  7241  subadd4  7253  mulneg12  7392  mulsub  7396  apreap  7576  cru  7591  recextlem1  7630  cju  7911  halfaddsub  8157  nn0supp  8232  nneo  8339  zeo2  8342  uzin  8503  iccf1o  8870  fzsuc2  8939  flqeqceilz  9158  frec2uzrdg  9169  iseqss  9200  iseqfveq2  9202  iseqsplit  9212  iseqdistr  9223  iser0f  9225  expp1  9236  mulexp  9268  mulexpzap  9269  expadd  9271  expaddzap  9273  expmul  9274  expmulzap  9275  expsubap  9276  expdivap  9279  subsq  9332  binom3  9340  bernneq  9343  shftval2  9401  shftval4  9403  crre  9431  remim  9434  remullem  9445  cjexp  9467  cnrecnv  9484  resqrexlemlo  9585  resqrexlemcalc1  9586  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnm  9590  rsqrmo  9599  abscj  9624  absid  9643  absre  9647  recvalap  9667  climaddc1  9823  climmulc2  9825  climsubc1  9826  climsubc2  9827  climcvg1nlem  9842  sqrt2irr  9852  ialgrp1  9859
  Copyright terms: Public domain W3C validator