Description: Join three consequents. (Contributed by FL, 1-Aug-2009)
Ref | Expression | ||
---|---|---|---|
Hypotheses | jca31.1 | |- ( ph -> ps ) |
|
jca31.2 | |- ( ph -> ch ) |
||
jca31.3 | |- ( ph -> th ) |
||
Assertion | jca32 | |- ( ph -> ( ps /\ ( ch /\ th ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca31.1 | |- ( ph -> ps ) |
|
2 | jca31.2 | |- ( ph -> ch ) |
|
3 | jca31.3 | |- ( ph -> th ) |
|
4 | 2 3 | jca | |- ( ph -> ( ch /\ th ) ) |
5 | 1 4 | jca | |- ( ph -> ( ps /\ ( ch /\ th ) ) ) |