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 φθψτχη

Proof

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