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

Theorem eqtrd 2150
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrd.1  |-  ( ph  ->  A  =  B )
eqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtrd  |-  ( ph  ->  A  =  C )

Proof of Theorem eqtrd
StepHypRef Expression
1 eqtrd.1 . 2  |-  ( ph  ->  A  =  B )
2 eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32eqeq2d 2129 . 2  |-  ( ph  ->  ( A  =  B  <-> 
A  =  C ) )
41, 3mpbid 146 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqtr2d  2151  eqtr3d  2152  eqtr4d  2153  3eqtrd  2154  3eqtrrd  2155  3eqtr2d  2156  syl5eq  2162  syl6eq  2166  rabeqbidv  2655  rabeqbidva  2656  csbidmg  3026  csbco3g  3028  difeq12d  3165  ifeq12d  3461  ifbieq1d  3464  ifbieq2d  3466  ifbieq12d  3468  eqifdc  3476  csbsng  3554  disjpr2  3557  csbunig  3714  iuneq12d  3807  unisn3  4336  op1stbg  4370  opthreg  4441  onsucuni2  4449  csbxpg  4590  coeq12d  4673  csbdmg  4703  reseq12d  4790  csbresg  4792  resima2  4823  imaeq12d  4852  csbrng  4970  opswapg  4995  relcnvtr  5028  relcoi2  5039  relcoi1  5040  iotaint  5071  funprg  5143  funtpg  5144  funcnvres2  5168  fnco  5201  fococnv2  5361  fveq12d  5396  csbfv12g  5425  csbfv2g  5426  csbfvg  5427  dffn5im  5435  funfvdm2  5453  fvun1  5455  fvmpt2d  5475  fvmptt  5480  fndmin  5495  fniniseg2  5510  fnniniseg2  5511  fmptcof  5555  fvresi  5581  fvunsng  5582  fvpr1g  5594  fvpr2g  5595  fvtp1g  5596  funiunfvdm  5632  fcof1o  5658  riotaeqbidv  5701  oveq123d  5763  csbov12g  5778  csbov1g  5779  csbov2g  5780  ovmpodxf  5864  caov42d  5925  caovdilemd  5930  caovimo  5932  grprinvd  5934  offeq  5963  offval2  5965  caofinvl  5972  ot1stg  6018  ot2ndg  6019  2nd1st  6046  mpomptsx  6063  dmmpossx  6065  fmpox  6066  fmpoco  6081  1stconst  6086  algrflemg  6095  tfrexlem  6199  rdgivallem  6246  rdgisuc1  6249  frec0g  6262  frecabcl  6264  frecsuclem  6271  frecrdg  6273  oa0  6321  oasuc  6328  oa1suc  6331  omsuc  6336  nnaass  6349  nndi  6350  nnmass  6351  nnm2  6389  nn2m  6390  ereq1  6404  errn  6419  uniqs2  6457  oviec  6503  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  mapsnconst  6556  mapen  6708  mapxpen  6710  xpmapenlem  6711  phplem4on  6729  fidifsnen  6732  undifdc  6780  fiintim  6785  fisseneq  6788  snexxph  6806  sbthlemi4  6816  sbthlemi6  6818  supeq2  6844  eqsupti  6851  infvalti  6877  djuf1olem  6906  djuss  6923  1stinl  6927  2ndinl  6928  1stinr  6929  2ndinr  6930  updjudhcoinlf  6933  updjudhcoinrg  6934  omp1eomlem  6947  difinfsn  6953  ctmlemr  6961  ctssdclemn0  6963  ctssdc  6966  enumctlemm  6967  en2other2  7020  mulidpi  7094  addasspig  7106  mulasspig  7108  distrpig  7109  indpi  7118  addcmpblnq  7143  mulpipq  7148  dmaddpqlem  7153  nqpi  7154  addcomnqg  7157  recrecnq  7170  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltaddnq  7183  ltexnqq  7184  archnqq  7193  prarloclemarch  7194  ltrnqg  7196  ltnnnq  7199  nq0nn  7218  addcmpblnq0  7219  nqpnq0nq  7229  nqnq0a  7230  nq0m0r  7232  nq0a0  7233  distrnq0  7235  addassnq0  7238  nq02m  7241  prarloclemlo  7270  prarloclemcalc  7278  addnqprllem  7303  addnqprulem  7304  addnqprl  7305  addnqpru  7306  appdivnq  7339  mulnqprl  7344  mulnqpru  7345  addcanprlemu  7391  ltaprlem  7394  ltmprr  7418  cauappcvgprlemladdrl  7433  mulcmpblnrlemg  7516  mulcomsrg  7533  distrsrg  7535  ltsosr  7540  1idsr  7544  00sr  7545  ltasrg  7546  recexgt0sr  7549  srpospr  7559  prsradd  7562  prsrriota  7564  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsrlemoffres  7576  caucvgsr  7578  map2psrprg  7581  elreal2  7606  mulresr  7614  pitonnlem1p1  7622  pitonnlem2  7623  pitoregt0  7625  recidpirqlemcalc  7633  recidpirq  7634  axaddcl  7640  axmulcl  7642  axmulcom  7647  axmulass  7649  axdistr  7650  ax1rid  7653  axcnre  7657  recriota  7666  axcaucvglemcau  7674  mulid1  7731  mulid2  7732  adddirp1d  7760  joinlmuladdmuld  7761  muladd11  7863  1p1times  7864  readdcan  7870  comraddd  7887  add42  7892  npcan  7939  addsubass  7940  2addsub  7944  addsubeq4  7945  nppcan  7952  nnpcan  7953  npncan2  7957  nncan  7959  subsub  7960  nnncan  7965  nnncan1  7966  pnpcan2  7970  pnncan  7971  subneg  7979  negneg  7980  negdi2  7988  mvrraddd  8096  assraddsubd  8098  subaddeqd  8099  addid0  8103  mul02  8117  mul01  8119  mulneg1  8125  mul2neg  8128  mulm1  8130  ltadd2  8149  rimul  8314  rereim  8315  mulreim  8333  recextlem1  8379  mulcanapd  8389  divcanap1  8408  divrecap2  8416  divmulassap  8422  divmulasscomap  8423  divcanap4  8426  dividap  8428  muldivdirap  8434  divdivdivap  8440  recdivap  8445  divadddivap  8454  divsubdivap  8455  div2negap  8462  divcanap5rd  8545  dmdcanap2d  8548  recgt0  8572  lt2mul2div  8601  nnmulcl  8705  times2  8807  add1p1  8927  sub1m1  8928  cnm2m1cnm3  8929  nn0supp  8987  peano2z  9048  nneoor  9111  supminfex  9348  cnref1o  9396  rexneg  9568  xaddpnf1  9584  xaddmnf1  9586  rexadd  9590  xaddid1  9600  xaddid2  9601  xaddass  9607  xpncan  9609  xleadd1a  9611  xltadd1  9614  xposdif  9620  xadd4d  9623  xleaddadd  9625  iooidg  9647  iooval2  9653  icoshftf1o  9729  lincmb01cmp  9741  iccf1o  9742  fzval2  9748  fzsuc  9804  fzpred  9805  fztpval  9818  fseq1p1m1  9829  fzshftral  9843  fzo0to3tp  9951  fzo0sn0fzo1  9953  fzosplitsn  9965  fzosplitprm1  9966  fzisfzounsn  9968  rebtwn2zlemstep  9985  2tnp1ge0ge0  10029  flqdiv  10049  modqvalr  10053  modqdiffl  10063  modqfrac  10065  modqmulnn  10070  modqid  10077  modqcyc  10087  modqcyc2  10088  mulp1mod1  10093  modqmuladd  10094  modqmuladdnn0  10096  qnegmod  10097  m1modnnsub1  10098  addmodid  10100  addmodidr  10101  modqmul12d  10106  modqnegd  10107  modqadd12d  10108  modifeq2int  10114  modqaddmulmod  10119  modqdi  10120  modqsubdir  10121  modsumfzodifsn  10124  addmodlteq  10126  frec2uzsucd  10129  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdglem  10139  frecuzrdgsuc  10142  frecuzrdgg  10144  frecuzrdgdomlem  10145  frecuzrdgfunlem  10147  frecuzrdgtclt  10149  frecuzrdgsuctlem  10151  frecfzennn  10154  seqeq1  10176  seq3val  10186  seqvalcd  10187  seq3p1  10190  seqp1cd  10194  seq3feq2  10198  seq3fveq  10199  seq3shft2  10201  seq3-1p  10208  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemnanb  10218  iseqf1olemqk  10222  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1o  10232  seq3id3  10235  seq3z  10239  fser0const  10244  exp3vallem  10249  expnnval  10251  expp1  10255  expn1ap0  10258  mulexp  10287  expaddzaplem  10291  expaddzap  10292  expmul  10293  expp1zap  10297  expm1ap  10298  sqval  10306  iexpcyc  10352  subsq2  10355  binom2  10358  binom21  10359  binom2sub1  10361  mulbinom2  10363  binom3  10364  zesq  10365  bernneq  10367  sqoddm1div8  10399  nn0opthlem1d  10421  facp1  10431  faclbnd6  10445  bcval2  10451  bcval3  10452  bcn0  10456  bcp1n  10462  bcp1nk  10463  bcn2  10465  bcp1m1  10466  bcpasc  10467  bcn2m1  10470  hashinfom  10479  hashennn  10481  hashfz1  10484  fseq1hash  10502  omgadd  10503  hashunsng  10508  hashprg  10509  hashdifsn  10520  hashdifpr  10521  hashfz  10522  hashfzo  10523  hashfzo0  10524  hashfzp1  10525  hashfz0  10526  hashxp  10527  resunimafz0  10529  fnfz0hash  10530  ffzo0hash  10532  hashfacen  10534  zfz1isolemsplit  10536  zfz1isolemiso  10537  zfz1isolem1  10538  shftdm  10549  shftval2  10553  shftval4  10555  shftval5  10556  shftcan1  10561  seq3shft  10565  imre  10578  crre  10584  remim  10587  reim0b  10589  recj  10594  reneg  10595  readd  10596  resub  10597  remullem  10598  imcj  10602  imneg  10603  imadd  10604  imsub  10605  cjcj  10610  cjadd  10611  ipcnval  10613  cjneg  10617  cjsub  10619  cjexp  10620  imval2  10621  cjap  10633  resqrexlemf1  10735  resqrexlemfp1  10736  resqrexlemover  10737  resqrexlemcalc1  10741  resqrexlemcalc3  10743  resqrexlemnm  10745  resqrexlemcvg  10746  resqrtcl  10756  sqrtsq  10771  absneg  10777  absvalsq  10780  absvalsq2  10781  sqabsadd  10782  sqabssub  10783  absval2  10784  absreimsq  10794  absmul  10796  absexp  10806  absexpzap  10807  abssuble0  10830  abstri  10831  recan  10836  amgm2  10845  maxabslemlub  10934  max0addsup  10946  minmax  10956  minabs  10962  bdtrilem  10965  bdtri  10966  xrmaxiflemab  10971  xrmaxiflemcom  10973  xrmaxadd  10985  xrminmax  10989  xrmineqinf  10993  xrminrecl  10997  xrbdtri  11000  climshft2  11030  subcn2  11035  reccn2ap  11037  climaddc2  11054  iser3shft  11070  climcvg1nlem  11073  sumeq12dv  11096  sumeq12rdv  11097  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  summodc  11107  fsum3  11111  isumz  11113  fsumf1o  11114  fisumss  11116  fsumsersdc  11119  fsum3ser  11121  fsumsplit  11131  fsumsplitf  11132  sumsnf  11133  fsumsplitsn  11134  fsum1  11136  sumpr  11137  sumtp  11138  fsumm1  11140  fsum1p  11142  fsumsplitsnun  11143  fsump1  11144  isumclim  11145  sumnul  11148  isumadd  11155  fsum2dlemstep  11158  fsumcnv  11161  fisumcom2  11162  fsumshftm  11169  fisumrev2  11170  fisum0diag2  11171  fsumsub  11176  fsumdifsnconst  11179  modfsummodlemstep  11181  fsumabs  11189  telfsumo  11190  telfsum  11192  telfsum2  11193  fsumparts  11194  fsumiun  11201  hashiun  11202  hash2iun  11203  hash2iun1dif1  11204  binomlem  11207  binom1p  11209  binom11  11210  binom1dif  11211  bcxmas  11213  isum1p  11216  isumnn0nn  11217  isumlessdc  11220  divcnv  11221  arisum2  11223  trireciplem  11224  geosergap  11230  geolim  11235  georeclim  11237  geo2lim  11240  geoisum1  11243  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemsumlt  11252  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  eftabs  11276  efcllemp  11278  ef0lem  11280  efcvgfsum  11287  ege2le3  11291  efcj  11293  efaddlem  11294  efexp  11302  eftlub  11310  efsep  11311  effsumlt  11312  ef4p  11314  efgt1p2  11315  efgt1p  11316  tanval2ap  11334  tanval3ap  11335  resinval  11336  recosval  11337  efi4p  11338  resin4p  11339  recos4p  11340  sinneg  11347  cosneg  11348  tannegap  11349  efmival  11354  sinadd  11357  cosadd  11358  tanaddaplem  11359  tanaddap  11360  sinsub  11361  cossub  11362  addsin  11363  subsin  11364  subcos  11368  sincossq  11369  sin2t  11370  sin01bnd  11378  cos01bnd  11379  absefi  11389  absef  11390  absefib  11391  efieq1re  11392  demoivre  11393  demoivreALT  11394  eirraplem  11395  dvdstr  11442  dvdsadd2b  11452  mulmoddvds  11473  ltoddhalfle  11502  opoe  11504  m1expo  11509  m1exp1  11510  flodddiv4  11543  flodddiv4t2lthalf  11546  zsupcllemstep  11550  nn0gcdid0  11581  gcdaddm  11584  gcdadd  11585  gcdid  11586  gcdabs  11588  modgcd  11591  1gcd  11592  bezout  11611  dfgcd2  11614  mulgcd  11616  absmulgcd  11617  gcdmultiple  11620  gcdmultiplez  11621  rpmulgcd  11626  rplpwr  11627  rppwr  11628  dvdssqlem  11630  ialgr0  11637  alginv  11640  algcvg  11641  algfx  11645  eucalginv  11649  eucalglt  11650  lcmcl  11665  lcmabs  11669  lcmgcdlem  11670  lcmdvds  11672  lcmgcdnn  11675  coprmdvds  11685  qredeq  11689  divgcdcoprm0  11694  divgcdcoprmex  11695  rpexp1i  11744  sqrt2irrlem  11751  sqpweven  11764  2sqpwodd  11765  sqrt2irraplemnn  11768  qmuldeneqnum  11784  nn0gcdsq  11789  numdensq  11791  nn0sqrtelqelz  11795  phibndlem  11803  dfphi2  11807  phiprmpw  11809  phiprm  11810  phimullem  11812  hashgcdlem  11814  ennnfonelemp1  11830  ennnfonelemhdmp1  11833  ennnfonelemss  11834  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemhom  11839  ennnfonelemnn0  11846  ctinfomlemom  11851  setsvala  11901  fvsetsid  11904  setsresg  11908  setscom  11910  setsslid  11920  ressid2  11929  ressval2  11930  restid2  12040  ntrval  12190  clsval  12191  cldcls  12194  neival  12223  resttop  12250  restco  12254  restabs  12255  resttopon2  12258  cnpval  12278  cnntr  12305  cnrest2  12316  upxp  12352  uptx  12354  cnmpt11  12363  cnmpt21  12371  psmetsym  12409  psmetres2  12413  xmetsym  12448  xmettxlem  12589  txmetcnp  12598  cnbl0  12614  cnblcld  12615  remetdval  12619  bl2ioo  12622  tgioo  12626  addcncntoplem  12631  divcnap  12635  fsumcncntop  12636  cncfmet  12659  cncfmptc  12662  addccncf  12666  negcncf  12668  mulcncflem  12670  ivthinclemlopn  12694  limcimolemlt  12713  cnplimcim  12716  cnplimclemr  12718  limccnp2lem  12725  limccnp2cntop  12726  dvfvalap  12730  dvconst  12741  dvaddxxbr  12745  dvmulxxbr  12746  dvcjbr  12752  dvexp  12755  dvrecap  12757  dvmptclx  12760  dvmptaddx  12761  dvmptmulx  12762  dvmptcmulcn  12763  dveflem  12766  dvef  12767  sin0pilem1  12773  sin0pilem2  12774  efper  12799  sinperlem  12800  sinmpi  12807  cosmpi  12808  sinppi  12809  cosppi  12810  efimpi  12811  ptolemy  12816  sinq12gt0  12822  coseq0negpitopi  12828  djucllem  12903  nninfalllemn  13098  nninfsellemeq  13106  nninffeq  13112  qdencn  13118  cvgcmp2nlemabs  13123  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator