Metamath Proof Explorer

Theorem im2anan9

Description: Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996)

Ref Expression
Hypotheses im2an9.1 φ ψ χ
im2an9.2 θ τ η
Assertion im2anan9 φ θ ψ τ χ η


Step Hyp Ref Expression
1 im2an9.1 φ ψ χ
2 im2an9.2 θ τ η
3 1 adantrd φ ψ τ χ
4 2 adantld θ ψ τ η
5 3 4 anim12ii φ θ ψ τ χ η