Metamath Proof Explorer

Theorem eqimsscd

Description: Equality implies inclusion, deduction version. (Contributed by SN, 15-Feb-2025)

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

Proof

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