Metamath Proof Explorer

Theorem jcad

Description: Deduction conjoining the consequents of two implications. Deduction form of jca and double deduction form of pm3.2 and pm3.2i . (Contributed by NM, 15-Jul-1993) (Proof shortened by Wolf Lammen, 23-Jul-2013)

Ref Expression
Hypotheses jcad.1 φ ψ χ
jcad.2 φ ψ θ
Assertion jcad φ ψ χ θ


Step Hyp Ref Expression
1 jcad.1 φ ψ χ
2 jcad.2 φ ψ θ
3 pm3.2 χ θ χ θ
4 1 2 3 syl6c φ ψ χ θ