Metamath Proof Explorer

Theorem eqimssd

Description: Equality implies inclusion, deduction version. (Contributed by SN, 6-Nov-2024)

Ref Expression
Hypothesis eqimssd.1 
|- ( ph -> A = B )
Assertion eqimssd 
|- ( ph -> A C_ B )

Proof

Step Hyp Ref Expression
1 eqimssd.1 
 |-  ( ph -> A = B )
2 ssid 
 |-  B C_ B
3 1 2 eqsstrdi 
 |-  ( ph -> A C_ B )