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

Metamath Proof Explorer

Theorem adantrd

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994)

		Ref	Expression
	Hypothesis	adantrd.1	$⊢ φ \to (ψ \to χ)$
	Assertion	adantrd	$⊢ φ \to ((ψ \land θ) \to χ)$

Step	Hyp	Ref	Expression
1		adantrd.1	$⊢ φ \to (ψ \to χ)$
2		simpl	$⊢ (ψ \land θ) \to ψ$
3	2 1	syl5	$⊢ φ \to ((ψ \land θ) \to χ)$