Metamath Proof Explorer


Theorem jca

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)

Ref Expression
Hypotheses jca.1 φ ψ
jca.2 φ χ
Assertion jca φ ψ χ

Proof

Step Hyp Ref Expression
1 jca.1 φ ψ
2 jca.2 φ χ
3 pm3.2 ψ χ ψ χ
4 1 2 3 sylc φ ψ χ