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 ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → ( 𝜒 ∧ 𝜑 ) ) ) )