Metamath Proof Explorer


Theorem anc2r

Description: Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion anc2r ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( 𝜑 → ( 𝜓 → ( 𝜒𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 pm3.21 ( 𝜑 → ( 𝜒 → ( 𝜒𝜑 ) ) )
2 1 imim2d ( 𝜑 → ( ( 𝜓𝜒 ) → ( 𝜓 → ( 𝜒𝜑 ) ) ) )
3 2 a2i ( ( 𝜑 → ( 𝜓𝜒 ) ) → ( 𝜑 → ( 𝜓 → ( 𝜒𝜑 ) ) ) )