Metamath Proof Explorer


Theorem a2i

Description: Inference distributing an antecedent. Inference associated with ax-2 . Its associated inference is mpd . (Contributed by NM, 29-Dec-1992)

Ref Expression
Hypothesis a2i.1 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion a2i ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) )

Proof

Step Hyp Ref Expression
1 a2i.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 ax-2 ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) )
3 1 2 ax-mp ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) )