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

Theorem eqtr2di 2190
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr2di.1
eqtr2di.2
Assertion
Ref Expression
eqtr2di

Proof of Theorem eqtr2di
StepHypRef Expression
1 eqtr2di.1 . . 3
2 eqtr2di.2 . . 3
31, 2eqtrdi 2189 . 2
43eqcomd 2146 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  eqtr4id  2192  elxp4  5036  elxp5  5037  fo1stresm  6069  fo2ndresm  6070  eloprabi  6104  fo2ndf  6134  xpsnen  6725  xpassen  6734  ac6sfi  6802  undifdc  6825  ine0  8203  nn0n0n1ge2  9168  fzval2  9847  fseq1p1m1  9928  fsum2dlemstep  11258  modfsummodlemstep  11281  ef4p  11460  sin01bnd  11523  odd2np1  11629  sqpweven  11912  2sqpwodd  11913  psmetdmdm  12555  xmetdmdm  12587  dveflem  12918  reeff1oleme  12924  abssinper  12998
 Copyright terms: Public domain W3C validator