This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem jctild

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005)

Ref Expression
Hypotheses jctild.1 ⊢ φ → ψ → χ
jctild.2 ⊢ φ → θ
Assertion jctild ⊢ φ → ψ → θ ∧ χ

Proof

Step Hyp Ref Expression
1 jctild.1 ⊢ φ → ψ → χ
2 jctild.2 ⊢ φ → θ
3 2 a1d ⊢ φ → ψ → θ
4 3 1 jcad ⊢ φ → ψ → θ ∧ χ