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

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

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2145 . 2 (𝜑𝐵 = 𝐴)
3 eqtr3d.2 . 2 (𝜑𝐴 = 𝐶)
42, 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:  3eqtr3d  2180  3eqtr3rd  2181  3eqtr3a  2196  opth  4159  eusvnf  4374  f00  5314  f1imacnv  5384  foimacnv  5385  f1ococnv1  5396  funfvdm  5484  fvmptdf  5508  fndmdif  5525  acexmidlemph  5767  acexmidlemab  5768  ovmpodf  5902  oprssov  5912  grpridd  5967  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  oav2  6359  omv2  6361  fnsnsplitdc  6401  ecopovtrn  6526  ecopovtrng  6529  map0b  6581  en1  6693  ssenen  6745  fidifsnen  6764  dif1en  6773  undifdc  6812  fidcenumlemr  6843  ordiso2  6920  finomni  7012  exmidomni  7014  fodjum  7018  exmidaclem  7069  distrnqg  7207  1qec  7208  prarloclemarch2  7239  nnnq0lem1  7266  nqpnq0nq  7273  distrnq0  7279  prarloclemlt  7313  prmuloclemcalc  7385  ltaprg  7439  prplnqu  7440  recexprlem1ssl  7453  recexprlem1ssu  7454  ltmprr  7462  cauappcvgprlemopl  7466  caucvgprlemopl  7489  caucvgprprlemopl  7517  caucvgprprlemexb  7527  prsrlem1  7562  ltsosr  7584  mulgt0sr  7598  recidpipr  7676  recriota  7710  nntopi  7714  axcaucvglemres  7719  addid2  7913  readdcan  7914  muladd11r  7930  add32r  7934  cnegexlem2  7950  cnegex  7952  pncan2  7981  addsubass  7984  subadd23  7986  addsub12  7987  subid  7993  subid1  7994  npncan  7995  nppcan3  7998  subsub  8004  nppcan2  8005  nnncan2  8011  npncan3  8012  pnpcan  8013  negdi  8031  mvlraddd  8138  mvlladdd  8139  pnpncand  8149  subdi  8159  mulsub  8175  mulsub2  8176  eqord1  8257  recexap  8426  div32ap  8464  divsubdirap  8480  divmuldivap  8484  divdivdivap  8485  divmuleqap  8489  divcanap6  8491  dmdcanap  8494  divsubdivap  8500  div2negap  8507  div2subap  8608  mvllmulapd  8613  prodgt0gt0  8621  cju  8731  zneo  9164  infrenegsupex  9401  qreccl  9446  mul2lt0rlt0  9558  xnpcan  9667  fzosn  9994  modqid  10134  modqm1p1mod0  10160  modqltm1p1mod  10161  modqmul1  10162  modaddmodup  10172  modaddmodlo  10173  modqsubdir  10178  iseqf1olemkle  10269  iseqf1olemklt  10270  seq3f1olemstep  10286  seq3f1oleml  10288  seqfeq3  10297  seq3distr  10298  expineg2  10314  expm1t  10333  expadd  10347  expaddzaplem  10348  expmulzap  10351  sqsubswap  10365  subsq2  10412  binom2sub  10417  binom3  10421  facndiv  10497  bcval5  10521  bcn2p1  10528  bcnm1  10530  2shfti  10615  shftcan2  10619  reim0  10645  imval2  10678  cjreim2  10688  cjdivap  10693  cnrecnv  10694  rennim  10786  resqrexlemnm  10802  remsqsqrt  10816  sqrtdiv  10826  sqrtmsq  10829  sqabsadd  10839  sqabssub  10840  absreim  10852  absdivap  10854  absnid  10857  sqabs  10866  abslt  10872  absle  10873  recvalap  10881  abssub  10885  maxabslemlub  10991  infxrnegsupex  11044  mulcn2  11093  reccn2ap  11094  cjcn2  11097  summodclem3  11161  summodclem2a  11162  summodc  11164  zsumdc  11165  fsum3  11168  fisumss  11173  fsumcl2lem  11179  fsumm1  11197  fsum1p  11199  isummulc2  11207  telfsumo  11247  binomlem  11264  bcxmas  11270  arisum  11279  trireciplem  11281  trirecip  11282  geolim2  11293  georeclim  11294  cvgratnnlemfm  11310  cvgratz  11313  mertenslemi1  11316  clim2divap  11321  prodmodclem3  11356  prodmodclem2a  11357  efcan  11394  efexp  11400  efzval  11401  efgt0  11402  eftlub  11408  efltim  11416  resinval  11433  recosval  11434  cosmul  11463  cos2t  11468  cos2tsin  11469  cos01bnd  11476  cos12dec  11485  eirraplem  11494  muldvds1  11529  dvdsexp  11570  oexpneg  11585  divalglemqt  11627  divalglemeunn  11629  divalglemeuneg  11631  divalgmod  11635  flodddiv4t2lthalf  11645  gcdid0  11679  gcdaddm  11683  dvdsgcdidd  11693  rpmulgcd  11725  sqgcd  11728  algcvg  11740  eucalgcvga  11750  eucalg  11751  dvdslcm  11761  lcmeq0  11763  lcmgcd  11770  qredeu  11789  sqnprm  11827  divgcdodd  11832  sqrt2irrlem  11850  sqpweven  11864  2sqpwodd  11865  divnumden  11885  hashdvds  11908  phimullem  11912  ennnfonelemhf1o  11937  strslssd  12019  topnidg  12147  restopnb  12364  txcnmpt  12456  cnmpt1t  12468  blhalf  12591  xmspropd  12660  mspropd  12661  limcimolemlt  12816  dvfre  12857  dveflem  12870  dvef  12871  sin2kpi  12914  cos2kpi  12915  sin2pim  12916  cos2pim  12917  ptolemy  12927  sincosq2sgn  12930  sincosq3sgn  12931  sincosq4sgn  12932  sinq12gt0  12933  tangtx  12941  sincosq1eq  12942  abssinper  12949  sinkpi  12950  relogeftb  12966  relogoprlem  12969  relogexp  12973  peano3nninf  13262  nninfsel  13274  nninffeq  13277  isomninnlem  13286  cvgcmp2nlemabs  13288  trilpolemlt1  13295  trirec0xor  13299
  Copyright terms: Public domain W3C validator