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

Metamath Proof Explorer

Theorem int3

Description: The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 is 3expia . (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		int3.1	$⊢ ((φ, ψ, χ) \to θ)$
2	1	dfvd3ani	$⊢ (φ \land ψ \land χ) \to θ$
3	2	3expia	$⊢ (φ \land ψ) \to (χ \to θ)$
4	3	dfvd2anir	$⊢ ((φ, ψ) \to (χ \to θ))$