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

Theorem eqtr2d 2173
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 2172 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2145 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  3eqtrrd  2177  3eqtr2rd  2179  ifandc  3508  onsucmin  4423  elxp4  5026  elxp5  5027  csbopeq1a  6086  ecinxp  6504  fundmen  6700  fidifsnen  6764  sbthlemi3  6847  ctm  6994  addpinq1  7286  1idsr  7590  prsradd  7608  cnegexlem3  7953  cnegex  7954  submul2  8175  mulsubfacd  8194  divadddivap  8501  infrenegsupex  9403  xadd4d  9682  fzval3  9995  fzoshftral  10029  ceiqm1l  10098  flqdiv  10108  flqmod  10125  intqfrac  10126  modqcyc2  10147  modqdi  10179  frecuzrdgtcl  10199  frecuzrdgfunlem  10206  seq3id2  10296  expnegzap  10341  binom2sub  10419  binom3  10423  fihashssdif  10578  reim  10638  mulreap  10650  addcj  10677  resqrexlemcalc1  10800  absimle  10870  infxrnegsupex  11046  clim2ser  11120  serf0  11135  summodclem3  11163  mptfzshft  11225  fsumrev  11226  fsum2mul  11236  isumsplit  11274  cvgratz  11315  mertenslemi1  11318  ef4p  11414  tanval3ap  11434  efival  11452  sinmul  11464  divalglemnn  11628  dfgcd2  11715  lcmgcdlem  11771  lcm1  11775  oddpwdclemxy  11860  oddpwdclemdc  11864  hashgcdeq  11917  ennnfonelemp1  11932  strslfvd  12016  cnclima  12408  dveflem  12872  tangtx  12943  abssinper  12951  reexplog  12976
  Copyright terms: Public domain W3C validator