List of all theorems which could be rewritten as transitivity property of used predicates

theorem :: ABCMIZ_A:50
 for t1,t2,t3 being expression of C st t1 matches_with t2 & t2 matches_with t3
  holds t1 matches_with t3;

theorem :: ABCMIZ_A:51
 for A1,A2,A3 being Subset of QuasiAdjs C
  st A1 matches_with A2 & A2 matches_with A3
  holds A1 matches_with A3;

theorem :: ABCMIZ_A:52
 for T1,T2,T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3
  holds T1 matches_with T3;

theorem :: ABSRED_0:3
  x =*=> y & y =*=> z implies x =*=> z;

theorem :: ABSRED_0:7
  x <=*=> y & y <=*=> z implies x <=*=> z;

theorem :: ABSRED_0:35
  x =+=> y & y =+=> z implies x =+=> z;

theorem :: ABSRED_0:58
  x <=+=> y & y <=+=> z implies x <=+=> z;

theorem :: ALG_1:14
  U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic;

theorem :: ALTCAT_2:8
  for I,J,K being set, A being ManySortedSet of I, B being ManySortedSet of J, 
      C being ManySortedSet of K holds A cc= B & B cc= C implies A cc= C;

theorem :: ALTCAT_3:8
  for C being category, o1,o2,o3 being Object of C st o1,o2 are_iso & o2,o3 are_iso 
   holds o1,o3 are_iso;

theorem :: ANPROJ_1:2
  are_Prop p,u & are_Prop u,q implies are_Prop p,q;

theorem :: ARMSTRNG:12
  for X being set, P, Q, S being Dependency of X st P <= Q & Q <= S holds P <= S;

theorem :: ARYTM_1:3
  x <=' y & y <=' z implies x <=' z;

theorem :: ARYTM_3:67
  r <=' s & s <=' t implies r <=' t;

theorem :: ASYMPT_3:33
  for f,g,h be Function of NAT,REAL
  st f negligibleEQ g & g negligibleEQ h
  holds f negligibleEQ h;

theorem :: AUTALG_1:10
  A is_transformable_to B & B is_transformable_to C implies 
  A is_transformable_to C;

theorem :: BAGORD_2:28
  for a,b,c being bag of I st a divides b divides c holds a divides c;

theorem :: BCIALG_5:1
  x <= y & y <= z implies x <= z;

theorem :: BHSP_3:12
  seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies
  seq1 is_compared_to seq3;

theorem :: BORSUK_3:3
  for S, T, V being non empty TopSpace st 
  S, T are_homeomorphic & T, V are_homeomorphic holds S, V are_homeomorphic;

theorem :: BORSUK_6:42
  a,b are_connected & b,c are_connected implies a,c are_connected;

theorem :: BORSUK_6:79
  for P, Q, R be Path of a, b holds P, Q are_homotopic & Q, R are_homotopic 
  implies P, R are_homotopic;

theorem :: CAT_1:60
  a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic;

theorem :: CAT_8:10
  for C1,C2,C3 being composable with_identities CategoryStr
  st C1 ~= C2 & C2 ~= C3 holds C1 ~= C3;

theorem :: CIRCTRM1:29
  for S1, S2, S3 being non empty ManySortedSign
  st S1, S2 are_equivalent & S2, S3 are_equivalent holds S1, S3 are_equivalent;

theorem :: CLOSURE3:4
  for A,B,C be set holds A is_coarser_than B & B is_coarser_than C
  implies A is_coarser_than C;

theorem :: CLVECT_2:68
  seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies 
  seq1 is_compared_to seq3;

theorem :: CQC_SIM1:46
  p,q are_similar & q,r are_similar implies p,r are_similar;

theorem :: CQC_THE3:6
  p |- q & q |- r implies p |- r;

theorem :: CQC_THE3:9
  X |- Y & Y |- Z implies X |- Z;

theorem :: CQC_THE3:19
  X |-| Y & Y |-| Z implies X |-| Z;

theorem :: CQC_THE3:28
  p |-| q & q |-| r implies p |-| r;

theorem :: CQC_THE3:51
  p <==> q & q <==> r implies p <==> r;

theorem :: DIST_1:6
  for S be finite set, s,t,u be FinSequence of S st
  s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
  s,u -are_prob_equivalent;

theorem :: EC_PF_1:44
  for p be Prime, P,Q,R be Element of ProjCo(GF(p)) holds
  P _EQ_ Q & Q _EQ_ R implies P _EQ_ R;

theorem :: EUCLIDLP:33
  x1 // x2 & x2 // x3 implies x1 // x3;

theorem :: EUCLIDLP:60
  L0 // L1 & L1 // L2 implies L0 // L2;

theorem :: FILTER_1:33
  for L1,L2,L3 being Lattice st L1,L2 are_isomorphic & L2,L3 are_isomorphic 
  holds L1,L3 are_isomorphic;

theorem :: FSM_1:15
  tfsm1, tfsm2-are_equivalent & tfsm2, tfsm3-are_equivalent
  implies tfsm1, tfsm3-are_equivalent;

theorem :: FSM_1:16
  q1, q2-are_equivalent & q2, q3-are_equivalent implies q1, q3 -are_equivalent;

theorem :: FSM_1:42
  tfsm1,tfsm2-are_isomorphic & tfsm2,tfsm3-are_isomorphic implies
  tfsm1,tfsm3-are_isomorphic;

theorem :: FUNCTOR2:2
  for A,B being transitive with_units non empty AltCatStr, F,F1,
  F2 being Functor of A,B holds F is_transformable_to F1 & F1
  is_transformable_to F2 implies F is_transformable_to F2;

theorem :: FUNCTOR2:8
  for A,B be category, F,F1,F2 be covariant Functor of A,B holds 
  F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies
  F is_naturally_transformable_to F2;

theorem :: FUNCTOR3:33
  F1, F2 are_naturally_equivalent & F2, F3 are_naturally_equivalent 
  implies F1, F3 are_naturally_equivalent;

theorem :: GAUSSINT:42
  for x, y, z be G_INTEG holds
  x is_associated_to y & y is_associated_to z implies x is_associated_to z;

theorem :: GCD_1:2
  for R being associative non empty multLoopStr 
  for a,b,c being Element of R holds a divides b & b divides c implies a divides c;

theorem :: GCD_1:4
  for R being associative non empty multLoopStr 
  for a,b,c being Element of R holds a is_associated_to b & b is_associated_to c implies 
  a is_associated_to c;

theorem :: GLIB_000:85
  G1 == G2 & G2 == G3 implies G1 == G3;

theorem :: GRAPH_1:17
  G1 c= G2 & G2 c= G3 implies G1 c= G3;

theorem :: GROUP_1A:276
  a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated;

theorem :: GROUP_1A:290
  A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated;

theorem :: GROUP_3:77
  a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated;

theorem :: GROUP_3:91
  A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated;

theorem :: GROUP_6:67
  G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic;

theorem :: GROUP_9:55
  G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic;

theorem :: INT_2:9
  a divides b & b divides c implies a divides c;

theorem :: ISOCAT_1:15
  A ~= B & B ~= C implies A ~= C;

theorem :: ISOCAT_1:46
  A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent;

theorem :: LANG1:8
  n1 is_derivable_from n2 & n2 is_derivable_from n3 implies 
  n1 is_derivable_from n3;

theorem :: LATTAD_1:25
  x [= y & y [= z implies x [= z;

theorem :: LATTICES:7
  for L being join-associative non empty \/-SemiLattStr, 
      a, b, c being Element of L holds a [= b & b [= c implies a [= c;

theorem :: LFUZZY_1:5
  for R,S,T being Membership_Func of X holds R c= S & S c= T implies R c= T;

theorem :: LMOD_6:18
  V c= M & M c= N implies V c= N;

theorem :: MATRIX10:45
  M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3;

theorem :: MATRIX_8:34
  M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3;

theorem :: METRIC_2:1
  for M being PseudoMetricSpace, x,y,z being Element of M holds 
  x tolerates y & y tolerates z implies x tolerates z;

theorem :: MFOLD_2:8
  A1,A2 are_homeomorphic & A2,A3 are_homeomorphic
  implies A1,A3 are_homeomorphic;

theorem :: MIDSP_1:23
  p ## q & q ## r implies p ## r;

theorem :: MODELC_2:34
  F is_proper_subformula_of G & G is_proper_subformula_of H
  implies F is_proper_subformula_of H;

theorem :: MODELC_2:35
  F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H;

theorem :: MSUALG_3:18
  for U1,U2,U3 being non-empty MSAlgebra over S holds 
  U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic;

theorem :: MSUHOM_1:5
  for S,S9,S99 be non empty ManySortedSign st S <= S9 & S9 <= S99 holds
  S <= S99;

theorem :: NAT_D:4
  i divides j & j divides h implies i divides h;

theorem :: NATTRA_1:18
  F is_transformable_to F1 & F1 is_transformable_to F2 implies 
  F is_transformable_to F2;

theorem :: NATTRA_1:23
  F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2
   implies F is_naturally_transformable_to F2;

theorem :: NATTRA_1:29
  F1 ~= F2 & F2 ~= F3 implies F1 ~= F3;

theorem :: NECKLACE:12
  for R,S,T be non empty RelStr holds R embeds S & S embeds T
  implies R embeds T;

theorem :: NECKLACE:13
  for R,S,T be non empty RelStr holds R is_equimorphic_to S & 
  S is_equimorphic_to T implies R is_equimorphic_to T;

theorem :: NELSON_1:15
  a <= b & b <= c implies a <= c;

theorem :: NORMFORM:2
  a c= b & b c= c implies a c= c;

theorem :: ORDERS_2:3
  for A being transitive RelStr, a1,a2,a3 being Element of A holds
  a1 <= a2 & a2 <= a3 implies a1 <= a3;

theorem :: ORDERS_2:5
  for A being transitive antisymmetric RelStr
   for a1,a2,a3 being Element of A holds a1 < a2 & a2 < a3 implies a1 < a3;

theorem :: ORDINAL1:10
  for A,B being set, C being epsilon-transitive set st A in B & B in C
   holds A in C;

theorem :: ORDINAL4:37
  A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C;

theorem :: OSALG_1:2
  for S being non empty non void OverloadedMSSign, 
      o,o1,o2 being OperSymbol of S holds o ~= o1 & o1 ~= o2 implies o ~= o2;

theorem :: OSALG_1:21
  for w1,w2,w3 being Element of (the carrier of S)* holds 
  w1 <= w2 & w2 <= w3 implies w1 <= w3;

theorem :: OSALG_1:23
  o1 <= o2 & o2 <= o3 implies o1 <= o3;

theorem :: OSALG_3:10
  for U1,U2,U3 being non-empty OSAlgebra of S1 holds 
  U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic;

theorem :: OSALG_4:3
  for R being non empty Poset, s1,s2,s3 being Element of R holds 
  s1 ~= s2 & s2 ~= s3 implies s1 ~= s3;

theorem :: PBOOLE:13
  X c= Y & Y c= Z implies X c= Z;

theorem :: PBOOLE:120
  X [= Y & Y [= Z implies X [= Z;

theorem :: PETERSON:9
  e1 <= e2 & e2 <= e3 implies e1 <= e3;

theorem :: PETERSON:12
  e1 << e2 & e2 << e3 implies e1 << e3;

theorem :: PNPROC_1:2
  m1 c= m2 & m2 c= m3 implies m1 c= m3;

theorem :: PRE_POLY:41
  for n being Ordinal, p, q, r being bag of n st p < q & q < r holds p < r;

theorem :: PRE_POLY:42
  for n being Ordinal, p, q, r being bag of n st p <=' q & q <=' r
  holds p <=' r;

theorem :: PUA2MSS1:30
  for S1,S2,S3 being ManySortedSign
  st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds S1 is_rougher_than S3;

theorem :: QC_LANG1:21
  s <= t & t <= u implies s <= u;

theorem :: QC_LANG2:56
  F is_proper_subformula_of G & G is_proper_subformula_of H
  implies F is_proper_subformula_of H;

theorem :: QC_LANG2:57
  F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H;

theorem :: QMAX_1:4
  p |- q & q |- r implies p |- r;

theorem :: QMAX_1:7
  p <==> q & q <==> r implies p <==> r;

theorem :: RING_3:44
  for R,S,T being Ring
  st R,S are_isomorphic & S,T are_isomorphic holds R,T are_isomorphic;

theorem :: RINGCAT1:5
  G1 <= G2 & G2 <= G3 implies G1 <= G3;

theorem :: ROUGHS_1:59
  X _c= Y & Y _c= Z implies X _c= Z;

theorem :: ROUGHS_1:60
  X c=^ Y & Y c=^ Z implies X c=^ Z;

theorem :: ROUGHS_1:61
  X _c=^ Y & Y _c=^ Z implies X _c=^ Z;

theorem :: RUSUB_5:3
  for V being Abelian add-associative right_zeroed
              right_complementable non empty RLSStruct
  for M,L,N be Affine Subset of V st
   M is_parallel_to L & L is_parallel_to N holds M is_parallel_to N;

theorem :: SETFAM_1:17
  SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ;

theorem :: SRINGS_5:74
  a <= b & b <= c implies a <= c;

theorem :: SRINGS_5:77
  a < b & b < c implies a < c;

theorem :: STACKS_1:13
  s1 == s2 & s2 == s3 implies s1 == s3;

theorem :: STACKS_1:46
  X1,X2 are_isomorphic & X2,X3 are_isomorphic implies X1,X3 are_isomorphic;

theorem :: UNIALG_2:2
  U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar;

theorem :: WAYBEL_1:7
  for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic
  holds L1,L3 are_isomorphic;

theorem :: WAYBEL_3:5
  for L being non empty Poset, x,y,z being Element of L
  st x << y & y << z holds x << z;

theorem :: WELLORD1:42
  R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic;

theorem :: WELLORD2:15
  X,Y are_equipotent & Y,Z are_equipotent implies X,Z are_equipotent;

theorem :: XBOOLE_1:1
  X c= Y & Y c= Z implies X c= Z;

theorem :: XBOOLE_1:56
  X c< Y & Y c< Z implies X c< Z;

theorem :: XXREAL_0:2
  for a,b,c being ExtReal holds
  a <= b & b <= c implies a <= c;

theorem :: YELLOW18:4
  for A,B,C being category st A,B are_equivalent & B,C are_equivalent
  holds A,C are_equivalent;

theorem :: YELLOW_4:4
  for L being transitive RelStr, A, B, C being Subset of L st 
  A is_finer_than B & B is_finer_than C holds A is_finer_than C;

theorem :: YELLOW_4:7
  for L being transitive RelStr, A, B, C being Subset of L st 
  C is_coarser_than B & B is_coarser_than A holds C is_coarser_than A;

theorem :: ZF_LANG:64
  F is_proper_subformula_of G & G is_proper_subformula_of H
  implies F is_proper_subformula_of H;

theorem :: ZF_LANG:65
  F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H;

theorem :: ZFREFLE1:19
  A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C;