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

Theorem eqtr2d 2115
 Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1 (𝜑𝐴 = 𝐵)
eqtr2d.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtr2d (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2d.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2114 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2087 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1285 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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-cleq 2075 This theorem is referenced by:  3eqtrrd  2119  3eqtr2rd  2121  onsucmin  4259  elxp4  4838  elxp5  4839  csbopeq1a  5845  ecinxp  6247  fundmen  6353  fidifsnen  6405  addpinq1  6716  1idsr  7007  prsradd  7024  cnegexlem3  7352  cnegex  7353  submul2  7570  mulsubfacd  7589  divadddivap  7882  infrenegsupex  8763  fzval3  9290  fzoshftral  9324  ceiqm1l  9393  flqdiv  9403  flqmod  9420  intqfrac  9421  modqcyc2  9442  modqdi  9474  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  iseqid2  9564  expnegzap  9607  binom2sub  9684  binom3  9687  reim  9877  mulreap  9889  addcj  9916  resqrexlemcalc1  10038  absimle  10108  clim2iser  10313  serif0  10327  divalglemnn  10462  dfgcd2  10547  lcmgcdlem  10603  lcm1  10607  oddpwdclemxy  10691  oddpwdclemdc  10695
 Copyright terms: Public domain W3C validator