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
|- ( ph -> ( ps -> ch ) )
im2an9.2
|- ( th -> ( ta -> et ) )
Assertion im2anan9
|- ( ( ph /\ th ) -> ( ( ps /\ ta ) -> ( ch /\ et ) ) )

Proof

Step Hyp Ref Expression
1 im2an9.1
 |-  ( ph -> ( ps -> ch ) )
2 im2an9.2
 |-  ( th -> ( ta -> et ) )
3 1 adantrd
 |-  ( ph -> ( ( ps /\ ta ) -> ch ) )
4 2 adantld
 |-  ( th -> ( ( ps /\ ta ) -> et ) )
5 3 4 anim12ii
 |-  ( ( ph /\ th ) -> ( ( ps /\ ta ) -> ( ch /\ et ) ) )