Metamath Proof Explorer
Description: An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24Nov2003)


Ref 
Expression 

Hypotheses 
ssini.1 
⊢ 𝐴 ⊆ 𝐵 


ssini.2 
⊢ 𝐴 ⊆ 𝐶 

Assertion 
ssini 
⊢ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

ssini.1 
⊢ 𝐴 ⊆ 𝐵 
2 

ssini.2 
⊢ 𝐴 ⊆ 𝐶 
3 
1 2

pm3.2i 
⊢ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) 
4 

ssin 
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ↔ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) ) 
5 
3 4

mpbi 
⊢ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 ) 