Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgred2 Structured version   Unicode version

Theorem efgred2 15390
 Description: Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w Word
efgval.r ~FG
efgval2.m
efgval2.t splice
efgred.d
efgred.s Word ..^
Assertion
Ref Expression
efgred2
Distinct variable groups:   ,   ,,,,,,,   ,   ,,,,,   ,,,,   ,,,,,,,,,   ,,,,,   ,,,,,,,,   ,,
Allowed substitution hints:   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   ()   (,,)

Proof of Theorem efgred2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . 8 Word
2 efgval.r . . . . . . . 8 ~FG
3 efgval2.m . . . . . . . 8
4 efgval2.t . . . . . . . 8 splice
5 efgred.d . . . . . . . 8
6 efgred.s . . . . . . . 8 Word ..^
71, 2, 3, 4, 5, 6efgsfo 15376 . . . . . . 7
8 fof 5656 . . . . . . 7
97, 8ax-mp 5 . . . . . 6
109ffvelrni 5872 . . . . 5
1110ad2antlr 709 . . . 4
121, 2, 3, 4, 5, 6efgredeu 15389 . . . 4
13 reurmo 2925 . . . 4
1411, 12, 133syl 19 . . 3
151, 2, 3, 4, 5, 6efgsdm 15367 . . . . 5 Word ..^
1615simp2bi 974 . . . 4
181, 2efger 15355 . . . . 5
1918a1i 11 . . . 4
201, 2, 3, 4, 5, 6efgsrel 15371 . . . . 5
2120ad2antrr 708 . . . 4
22 simpr 449 . . . 4
2319, 21, 22ertrd 6924 . . 3
241, 2, 3, 4, 5, 6efgsdm 15367 . . . . 5 Word ..^
2524simp2bi 974 . . . 4
271, 2, 3, 4, 5, 6efgsrel 15371 . . . 4