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

Theorem eqtr2d 2151
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1  |-  ( ph  ->  A  =  B )
eqtr2d.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtr2d  |-  ( ph  ->  C  =  A )

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 eqtr2d.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2150 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2123 1  |-  ( ph  ->  C  =  A )
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:  3eqtrrd  2155  3eqtr2rd  2157  ifandc  3478  onsucmin  4393  elxp4  4996  elxp5  4997  csbopeq1a  6054  ecinxp  6472  fundmen  6668  fidifsnen  6732  sbthlemi3  6815  ctm  6962  addpinq1  7240  1idsr  7544  prsradd  7562  cnegexlem3  7907  cnegex  7908  submul2  8129  mulsubfacd  8148  divadddivap  8455  infrenegsupex  9357  xadd4d  9636  fzval3  9949  fzoshftral  9983  ceiqm1l  10052  flqdiv  10062  flqmod  10079  intqfrac  10080  modqcyc2  10101  modqdi  10133  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  seq3id2  10250  expnegzap  10295  binom2sub  10373  binom3  10377  fihashssdif  10532  reim  10592  mulreap  10604  addcj  10631  resqrexlemcalc1  10754  absimle  10824  infxrnegsupex  11000  clim2ser  11074  serf0  11089  summodclem3  11117  mptfzshft  11179  fsumrev  11180  fsum2mul  11190  isumsplit  11228  cvgratz  11269  mertenslemi1  11272  ef4p  11327  tanval3ap  11348  efival  11366  sinmul  11378  divalglemnn  11542  dfgcd2  11629  lcmgcdlem  11685  lcm1  11689  oddpwdclemxy  11774  oddpwdclemdc  11778  hashgcdeq  11831  ennnfonelemp1  11846  strslfvd  11927  cnclima  12319  dveflem  12782  tangtx  12846  abssinper  12854
  Copyright terms: Public domain W3C validator