It's the second time now I got ex-natded5.3i into my proof on minimize!
Since it seems that this is a very useful theorem, I want to propose to put it into the first part of
set.mm (maybe after ~ jctir), in the following form:
${
jccir.1 $e |- ( ph -> ps ) $.
jccir.2 $e |- ( ps -> ch ) $.
$( Inference conjoining a consequent of a consequent to right of the
consequent in an implication. (Contributed by Mario Carneiro,
9-Feb-2017.) $)
jccir $p |- ( ph -> ( ps /\ ch ) ) $=
( syl jca ) ABCDABCDEFG $.
$}
In my special case, the following segment of a proof (7 lines)
65 rnggrp $p |- ( R e. Ring -> R e. Grp )
66 rnggrp $p |- ( R e. Ring -> R e. Grp )
67 eqid $p |- ( Base ` R ) = ( Base ` R )
68 d1matid.0 $e |- .0. = ( 0g ` R )
69 67,68 grpidcl $p |- ( R e. Grp -> .0. e. ( Base ` R ) )
70 66,69 syl $p |- ( R e. Ring -> .0. e. ( Base ` R ) )
71 65,70 jca $p |- ( R e. Ring -> ( R e. Grp /\ .0. e. ( Base ` R ) ) )
was replaced by the following segment (5 lines):
5326 rnggrp $p |- ( R e. Ring -> R e. Grp )
5335 eqid $p |- ( Base ` R ) = ( Base ` R )
5336 d1matid.0 $e |- .0. = ( 0g ` R )
5337 5335,5336 grpidcl $p |- ( R e. Grp -> .0. e. ( Base ` R ) )
5338 5326,5337 ex-natded5.3i $p |- ( R e. Ring -> ( R e. Grp /\ .0. e. ( Base` R ) ) )