Description: Deduce conjunction of the consequents of two implications ("join
consequents with 'and'"). Deduction form of pm3.2 and pm3.2i . Its
associated deduction is jcad . Equivalent to the natural deduction
rule /\ I ( /\ introduction), see natded . (Contributed by NM, 3-Jan-1993)(Proof shortened by Wolf Lammen, 25-Oct-2012)