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

Metamath Proof Explorer

Theorem jctil

Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993)

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

Proof

Step Hyp Ref Expression
1 jctil.1 ⊢ φ → ψ
2 jctil.2 ⊢ χ
3 2 a1i ⊢ φ → χ
4 3 1 jca ⊢ φ → χ ∧ ψ