Metamath Proof Explorer


Theorem ssinss1OLD

Description: Obsolete version of ssinss1 as of 10-Jun-2026. (Contributed by NM, 14-Sep-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssinss1OLD A C A B C

Proof

Step Hyp Ref Expression
1 inss1 A B A
2 sstr2 A B A A C A B C
3 1 2 ax-mp A C A B C