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

Theorem eqtr3d 2175
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr3d.1  |-  ( ph  ->  A  =  B )
eqtr3d.2  |-  ( ph  ->  A  =  C )
Assertion
Ref Expression
eqtr3d  |-  ( ph  ->  B  =  C )

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2146 . 2  |-  ( ph  ->  B  =  A )
3 eqtr3d.2 . 2  |-  ( ph  ->  A  =  C )
42, 3eqtrd 2173 1  |-  ( ph  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  3eqtr3d  2181  3eqtr3rd  2182  3eqtr3a  2197  opth  4166  eusvnf  4381  f00  5321  f1imacnv  5391  foimacnv  5392  f1ococnv1  5403  funfvdm  5491  fvmptdf  5515  fndmdif  5532  acexmidlemph  5774  acexmidlemab  5775  ovmpodf  5909  oprssov  5919  grpridd  5974  tfrlemisucaccv  6229  tfr1onlemsucaccv  6245  tfrcllemsucaccv  6258  oav2  6366  omv2  6368  fnsnsplitdc  6408  ecopovtrn  6533  ecopovtrng  6536  map0b  6588  en1  6700  ssenen  6752  fidifsnen  6771  dif1en  6780  undifdc  6819  fidcenumlemr  6850  ordiso2  6927  finomni  7019  exmidomni  7021  fodjum  7025  exmidaclem  7080  distrnqg  7218  1qec  7219  prarloclemarch2  7250  nnnq0lem1  7277  nqpnq0nq  7284  distrnq0  7290  prarloclemlt  7324  prmuloclemcalc  7396  ltaprg  7450  prplnqu  7451  recexprlem1ssl  7464  recexprlem1ssu  7465  ltmprr  7473  cauappcvgprlemopl  7477  caucvgprlemopl  7500  caucvgprprlemopl  7528  caucvgprprlemexb  7538  prsrlem1  7573  ltsosr  7595  mulgt0sr  7609  recidpipr  7687  recriota  7721  nntopi  7725  axcaucvglemres  7730  addid2  7924  readdcan  7925  muladd11r  7941  add32r  7945  cnegexlem2  7961  cnegex  7963  pncan2  7992  addsubass  7995  subadd23  7997  addsub12  7998  subid  8004  subid1  8005  npncan  8006  nppcan3  8009  subsub  8015  nppcan2  8016  nnncan2  8022  npncan3  8023  pnpcan  8024  negdi  8042  mvlraddd  8149  mvlladdd  8150  pnpncand  8160  subdi  8170  mulsub  8186  mulsub2  8187  eqord1  8268  recexap  8437  div32ap  8475  divsubdirap  8491  divmuldivap  8495  divdivdivap  8496  divmuleqap  8500  divcanap6  8502  dmdcanap  8505  divsubdivap  8511  div2negap  8518  div2subap  8619  mvllmulapd  8624  prodgt0gt0  8632  cju  8742  zneo  9175  infrenegsupex  9415  qreccl  9460  mul2lt0rlt0  9575  xnpcan  9684  fzosn  10012  modqid  10152  modqm1p1mod0  10178  modqltm1p1mod  10179  modqmul1  10180  modaddmodup  10190  modaddmodlo  10191  modqsubdir  10196  iseqf1olemkle  10287  iseqf1olemklt  10288  seq3f1olemstep  10304  seq3f1oleml  10306  seqfeq3  10315  seq3distr  10316  expineg2  10332  expm1t  10351  expadd  10365  expaddzaplem  10366  expmulzap  10369  sqsubswap  10383  subsq2  10430  binom2sub  10435  binom3  10439  facndiv  10516  bcval5  10540  bcn2p1  10547  bcnm1  10549  2shfti  10634  shftcan2  10638  reim0  10664  imval2  10697  cjreim2  10707  cjdivap  10712  cnrecnv  10713  rennim  10805  resqrexlemnm  10821  remsqsqrt  10835  sqrtdiv  10845  sqrtmsq  10848  sqabsadd  10858  sqabssub  10859  absreim  10871  absdivap  10873  absnid  10876  sqabs  10885  abslt  10891  absle  10892  recvalap  10900  abssub  10904  maxabslemlub  11010  infxrnegsupex  11063  mulcn2  11112  reccn2ap  11113  cjcn2  11116  summodclem3  11180  summodclem2a  11181  summodc  11183  zsumdc  11184  fsum3  11187  fisumss  11192  fsumcl2lem  11198  fsumm1  11216  fsum1p  11218  isummulc2  11226  telfsumo  11266  binomlem  11283  bcxmas  11289  arisum  11298  trireciplem  11300  trirecip  11301  geolim2  11312  georeclim  11313  cvgratnnlemfm  11329  cvgratz  11332  mertenslemi1  11335  clim2divap  11340  prodmodclem3  11375  prodmodclem2a  11376  zproddc  11379  efcan  11417  efexp  11423  efzval  11424  efgt0  11425  eftlub  11431  efltim  11439  resinval  11456  recosval  11457  cosmul  11486  cos2t  11491  cos2tsin  11492  cos01bnd  11499  cos12dec  11508  eirraplem  11517  muldvds1  11552  dvdsexp  11593  oexpneg  11608  divalglemqt  11650  divalglemeunn  11652  divalglemeuneg  11654  divalgmod  11658  flodddiv4t2lthalf  11668  gcdid0  11702  gcdaddm  11706  dvdsgcdidd  11716  rpmulgcd  11748  sqgcd  11751  algcvg  11763  eucalgcvga  11773  eucalg  11774  dvdslcm  11784  lcmeq0  11786  lcmgcd  11793  qredeu  11812  sqnprm  11850  divgcdodd  11855  sqrt2irrlem  11873  sqpweven  11887  2sqpwodd  11888  divnumden  11908  hashdvds  11931  phimullem  11935  ennnfonelemhf1o  11960  strslssd  12042  topnidg  12170  restopnb  12387  txcnmpt  12479  cnmpt1t  12491  blhalf  12614  xmspropd  12683  mspropd  12684  limcimolemlt  12839  dvfre  12880  dveflem  12893  dvef  12894  sin2kpi  12938  cos2kpi  12939  sin2pim  12940  cos2pim  12941  ptolemy  12951  sincosq2sgn  12954  sincosq3sgn  12955  sincosq4sgn  12956  sinq12gt0  12957  tangtx  12965  sincosq1eq  12966  abssinper  12973  sinkpi  12974  relogeftb  12992  relogoprlem  12995  relogexp  12999  peano3nninf  13374  nninfsel  13386  nninffeq  13389  isomninnlem  13398  cvgcmp2nlemabs  13400  trilpolemlt1  13407  trirec0xor  13411  ismkvnnlem  13417
  Copyright terms: Public domain W3C validator