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

Theorem eqtr2d 2121
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 2120 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2093 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  3eqtrrd  2125  3eqtr2rd  2127  ifandc  3427  onsucmin  4324  elxp4  4918  elxp5  4919  csbopeq1a  5958  ecinxp  6367  fundmen  6523  fidifsnen  6586  sbthlemi3  6668  addpinq1  7023  1idsr  7314  prsradd  7331  cnegexlem3  7659  cnegex  7660  submul2  7877  mulsubfacd  7896  divadddivap  8194  infrenegsupex  9082  fzval3  9615  fzoshftral  9649  ceiqm1l  9718  flqdiv  9728  flqmod  9745  intqfrac  9746  modqcyc2  9767  modqdi  9799  frecuzrdgtcl  9819  frecuzrdgfunlem  9826  seq3id2  9940  iseqid2  9941  expnegzap  9989  binom2sub  10067  binom3  10071  fihashssdif  10226  reim  10286  mulreap  10298  addcj  10325  resqrexlemcalc1  10447  absimle  10517  clim2ser  10725  serf0  10741  isummolem3  10770  mptfzshft  10836  fsumrev  10837  fsum2mul  10847  isumsplit  10885  cvgratz  10926  mertenslemi1  10929  ef4p  10984  tanval3ap  11005  efival  11023  sinmul  11035  divalglemnn  11196  dfgcd2  11281  lcmgcdlem  11337  lcm1  11341  oddpwdclemxy  11425  oddpwdclemdc  11429  hashgcdeq  11482  strslfvd  11535
  Copyright terms: Public domain W3C validator