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

Metamath Proof Explorer

Theorem 3impcombi

Description: A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017)

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

Step	Hyp	Ref	Expression
1		3impcombi.1	$⊢ (φ \land ψ \land φ) \to (χ \leftrightarrow θ)$
2	1	biimpd	$⊢ (φ \land ψ \land φ) \to (χ \to θ)$
3	2	3anidm13	$⊢ (φ \land ψ) \to (χ \to θ)$
4	3	ancoms	$⊢ (ψ \land φ) \to (χ \to θ)$
5	4	3impia	$⊢ (ψ \land φ \land χ) \to θ$