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 ) ) ) |
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 ) ) ) |