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

Theorem eqtr2d 2211
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 2210 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2183 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  3eqtrrd  2215  3eqtr2rd  2217  ifandc  3571  ifordc  3572  onsucmin  4503  elxp4  5112  elxp5  5113  csbopeq1a  6183  ecinxp  6604  fundmen  6800  fidifsnen  6864  sbthlemi3  6952  ctm  7102  addpinq1  7451  1idsr  7755  prsradd  7773  cnegexlem3  8121  cnegex  8122  submul2  8343  mulsubfacd  8362  divadddivap  8670  infrenegsupex  9580  xadd4d  9869  fzval3  10187  fzoshftral  10221  ceiqm1l  10294  flqdiv  10304  flqmod  10321  intqfrac  10322  modqcyc2  10343  modqdi  10375  frecuzrdgtcl  10395  frecuzrdgfunlem  10402  seq3id2  10492  expnegzap  10537  binom2sub  10616  binom3  10620  fihashssdif  10779  reim  10842  mulreap  10854  addcj  10881  resqrexlemcalc1  11004  absimle  11074  infxrnegsupex  11252  clim2ser  11326  serf0  11341  summodclem3  11369  mptfzshft  11431  fsumrev  11432  fsum2mul  11442  isumsplit  11480  cvgratz  11521  mertenslemi1  11524  fprodrev  11608  ef4p  11683  tanval3ap  11703  efival  11721  sinmul  11733  divalglemnn  11903  dfgcd2  11995  lcmgcdlem  12057  lcm1  12061  oddpwdclemxy  12149  oddpwdclemdc  12153  eulerthlemth  12212  hashgcdeq  12219  powm2modprm  12232  pythagtriplem16  12259  pczpre  12277  pcqdiv  12287  pcadd  12319  pcfac  12328  4sqlem10  12365  ennnfonelemp1  12387  strslfvd  12483  grpinvssd  12833  grpinvval2  12839  opprringbg  13072  ringinvdv  13134  cnclima  13383  dveflem  13847  tangtx  13919  abssinper  13927  reexplog  13952  rprelogbdiv  14035  lgsdirnn0  14108  lgsdinn0  14109  2sqlem2  14111  mul2sq  14112
  Copyright terms: Public domain W3C validator