Description: Infer conjunction of premises. Inference associated with pm3.2 . Its associated deduction is jca (and the double deduction is jcad ). (Contributed by NM, 21-Jun-1993)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pm3.2i.1 | |- ph |
|
pm3.2i.2 | |- ps |
||
Assertion | pm3.2i | |- ( ph /\ ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2i.1 | |- ph |
|
2 | pm3.2i.2 | |- ps |
|
3 | pm3.2 | |- ( ph -> ( ps -> ( ph /\ ps ) ) ) |
|
4 | 1 2 3 | mp2 | |- ( ph /\ ps ) |