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 φ ψ χ φ ψ χ φ


Step Hyp Ref Expression
1 pm3.21 φ χ χ φ
2 1 imim2d φ ψ χ ψ χ φ
3 2 a2i φ ψ χ φ ψ χ φ