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

Theorem eqtr4d 2175
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 2145 . 2 (𝜑𝐵 = 𝐶)
41, 3eqtrd 2172 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  3eqtr2d  2178  3eqtr2rd  2179  3eqtr4d  2182  3eqtr4rd  2183  3eqtr4a  2198  sbnfc2  3060  ifsbdc  3486  ifeq1dadc  3502  eqifdc  3506  ifandc  3508  onsucuni2  4479  relop  4689  riinint  4800  iotauni  5100  fniinfv  5479  fsn2  5594  fmptapd  5611  fconst2g  5635  fniunfv  5663  ofres  5996  ofco  6000  frecsuclem  6303  frecrdg  6305  oasuc  6360  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  funresdfunsndc  6402  uniqs2  6489  en1bg  6694  fundmen  6700  1domsn  6713  mapxpen  6742  xpmapenlem  6743  phplem4dom  6756  en2eqpr  6801  sbthlemi5  6849  omp1eomlem  6979  difinfsnlem  6984  ctmlemr  6993  ctssdccl  6996  ctssdc  6998  infnninf  7022  exmidonfinlem  7054  addcmpblnq  7187  distrnqg  7207  ltexnqq  7228  addcmpblnq0  7263  nqnq0a  7274  nqnq0m  7275  nq0m0r  7276  nq0a0  7277  nnanq0  7278  distrnq0  7279  prarloclemlo  7314  prarloclemcalc  7322  genpassl  7344  genpassu  7345  ltsosr  7584  0idsr  7587  1idsr  7588  mulextsr1lem  7600  cnegex  7952  subsub3  8006  subadd4  8018  mulneg12  8171  mulsub  8175  apreap  8361  cru  8376  recextlem1  8424  cju  8731  halfaddsub  8966  nn0supp  9041  nneo  9166  zeo2  9169  uzin  9370  xaddcom  9656  xaddass  9664  xleaddadd  9682  iccf1o  9799  fzsuc2  9871  flqeqceilz  10103  zmod1congr  10126  modqcyc  10144  modqcyc2  10145  modqaddabs  10147  modqmul1  10162  modqaddmulmod  10176  addmodlteq  10183  frec2uzrdg  10194  frecuzrdgsuctlem  10208  seq3val  10243  seqvalcd  10244  seq3fveq2  10254  seq3split  10264  seq3distr  10298  ser0f  10300  expp1  10312  mulexp  10344  mulexpzap  10345  expadd  10347  expaddzap  10349  expmul  10350  expmulzap  10351  expsubap  10353  expdivap  10356  subsq  10411  mulbinom2  10420  binom3  10421  bernneq  10424  nn0opthd  10480  faclbnd  10499  faclbnd6  10502  bccmpl  10512  bcp1n  10519  zfz1isolemiso  10594  seq3coll  10597  shftval2  10610  shftval4  10612  seq3shft  10622  crre  10641  remim  10644  remullem  10655  cjexp  10677  cnrecnv  10694  resqrexlemlo  10797  resqrexlemcalc1  10798  resqrexlemcalc2  10799  resqrexlemcalc3  10800  resqrexlemnm  10802  rsqrmo  10811  abscj  10836  absid  10855  absre  10861  recvalap  10881  maxabsle  10988  maxltsup  11002  2zsupmax  11009  minabs  11019  bdtrilem  11022  bdtri  11023  xrmaxiflemab  11028  xrmaxiflemcom  11030  xrmaxadd  11042  xrbdtri  11057  iooinsup  11058  climaddc1  11110  climmulc2  11112  climsubc1  11113  climsubc2  11114  climcvg1nlem  11130  summodclem3  11161  zsumdc  11165  isum  11166  isumz  11170  isumss  11172  fisumss  11173  fsum3cvg2  11175  fsumadd  11187  isummulc2  11207  sumsplitdc  11213  fsum2dlemstep  11215  fisumcom2  11219  fisum0diag2  11228  fsumconst  11235  telfsumo  11247  fsumparts  11251  fsumrelem  11252  binomlem  11264  isumshft  11271  isumsplit  11272  arisum  11279  arisum2  11280  trireciplem  11281  geolim2  11293  geo2sum  11295  0.999...  11302  cvgratz  11313  mertensabs  11318  clim2prod  11320  prodf1f  11324  prodmodclem2a  11357  ef0lem  11378  efval2  11383  ege2le3  11389  efaddlem  11392  efsub  11399  eftlub  11408  efsep  11409  tanval3ap  11432  efi4p  11435  sinneg  11444  sinmul  11462  sincossq  11466  cos2t  11468  demoivreALT  11491  eirraplem  11494  odd2np1  11581  omoe  11604  divalglemex  11630  divalglemeuneg  11631  divalgmod  11635  flodddiv4  11642  gcdneg  11681  gcdaddm  11683  modgcd  11690  bezoutlemnewy  11695  gcdass  11714  gcdmultiple  11719  algrp1  11738  lcmneg  11766  lcmgcdeq  11775  lcmass  11777  cncongr2  11796  prmexpb  11840  sqrt2irr  11851  2sqpwodd  11865  qnumdenbi  11881  phiprmpw  11909  ctiunctlemfo  11963  strslfv3  12018  restuni2  12360  lmfval  12375  cnfval  12377  cnpfval  12378  txtopon  12445  txcnp  12454  upxp  12455  txrest  12459  cnmptcom  12481  bl2in  12586  xblss2  12588  isxms2  12635  setsmsdsg  12663  setsmstsetg  12664  metss  12677  resubmet  12731  cncfcncntop  12763  dvidlemap  12843  dvcnp2cntop  12846  dvcoapbr  12854  dvcjbr  12855  dvexp  12858  dvexp2  12859  dvrecap  12860  efimpi  12922  tangtx  12941  logdivlti  12981  cxpexprp  12995  rpcxpsub  13008  sssneq  13281  0nninf  13283  nninfalllemn  13288  trilpolemisumle  13317
  Copyright terms: Public domain W3C validator