Metamath Proof Explorer
Theorem a2i
Description: Inference distributing an antecedent. Inference associated with
ax2 . Its associated inference is mpd . (Contributed by NM, 29Dec1992)


Ref 
Expression 

Hypothesis 
a2i.1 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 

Assertion 
a2i 
⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

a2i.1 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 
2 

ax2 
⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) ) 
3 
1 2

axmp 
⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) 