Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of WhiteheadRussell p. 111. Its associated inference is pm3.2i and its associated deduction is jca (and the double deduction is jcad ). See pm3.2im for a version using only implication and negation. (Contributed by NM, 5Jan1993) (Proof shortened by Wolf Lammen, 12Nov2012)
Ref  Expression  

Assertion  pm3.2   ( ph > ( ps > ( ph /\ ps ) ) ) 
Step  Hyp  Ref  Expression 

1  id   ( ( ph /\ ps ) > ( ph /\ ps ) ) 

2  1  ex   ( ph > ( ps > ( ph /\ ps ) ) ) 