Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  syl6c

Theorem syl6c 25
Description: A contractive variant of syl6 24 (Contributed by la korvo, 31-Jul-2023.)
Hypotheses
Ref Expression
syl6c.0ganai broda gi ganai brode gi brodi
syl6c.1ganai broda gi ganai brode gi brodo
syl6c.2ganai brodi gi ganai brodo gi brodu
Assertion
Ref Expression
syl6cganai broda gi ganai brode gi brodu

Proof of Theorem syl6c
StepHypRef Expression
1 syl6c.1 . 2ganai broda gi ganai brode gi brodo
2 syl6c.0 . . 3ganai broda gi ganai brode gi brodi
3 syl6c.2 . . 3ganai brodi gi ganai brodo gi brodu
42, 3syl6 24 . 2ganai broda gi ganai brode gi ganai brodo gi brodu
51, 4mpdd 22 1ganai broda gi ganai brode gi brodu
Colors of variables: sumti selbri bridi
Syntax hints:  ganai bgan 9
This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15
This theorem is referenced by:  syldd  38  isodd  70
  Copyright terms: Public domain W3C validator