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

Theorem eqtr2d 2223
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 2222 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2195 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  3eqtrrd  2227  3eqtr2rd  2229  ifandc  3587  ifordc  3588  onsucmin  4527  elxp4  5137  elxp5  5138  csbopeq1a  6217  ecinxp  6640  fundmen  6836  fidifsnen  6902  sbthlemi3  6992  ctm  7142  addpinq1  7498  1idsr  7802  prsradd  7820  cnegexlem3  8170  cnegex  8171  submul2  8392  mulsubfacd  8411  divadddivap  8720  infrenegsupex  9631  xadd4d  9922  fzval3  10241  fzoshftral  10275  ceiqm1l  10349  flqdiv  10359  flqmod  10376  intqfrac  10377  modqcyc2  10398  modqdi  10430  frecuzrdgtcl  10450  frecuzrdgfunlem  10457  seq3id2  10549  expnegzap  10595  binom2sub  10675  binom3  10679  fihashssdif  10840  reim  10903  mulreap  10915  addcj  10942  resqrexlemcalc1  11065  absimle  11135  infxrnegsupex  11313  clim2ser  11387  serf0  11402  summodclem3  11430  mptfzshft  11492  fsumrev  11493  fsum2mul  11503  isumsplit  11541  cvgratz  11582  mertenslemi1  11585  fprodrev  11669  ef4p  11744  tanval3ap  11764  efival  11782  sinmul  11794  divalglemnn  11965  dfgcd2  12057  lcmgcdlem  12121  lcm1  12125  oddpwdclemxy  12213  oddpwdclemdc  12217  eulerthlemth  12276  hashgcdeq  12283  powm2modprm  12296  pythagtriplem16  12323  pczpre  12341  pcqdiv  12351  pcadd  12384  pcfac  12394  4sqlem10  12431  4sqlem19  12453  ennnfonelemp1  12469  strslfvd  12566  xpsff1o  12837  gsumsplit1r  12885  grpinvssd  13045  grpinvval2  13051  opprrngbg  13454  opprringbg  13456  ringinvdv  13521  lss1d  13725  cnclima  14209  divcncfap  14586  dveflem  14690  tangtx  14762  abssinper  14770  reexplog  14795  rprelogbdiv  14878  lgsdirnn0  14952  lgsdinn0  14953  lgseisenlem2  14955  2sqlem2  14966  mul2sq  14967
  Copyright terms: Public domain W3C validator