Metamath Proof Explorer

Theorem bi13impib

Description: 3impib with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017)

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

Step	Hyp	Ref	Expression
1		bi13impib.1	$⊢ φ \leftrightarrow ((ψ \land χ) \to θ)$
2	1	biimpi	$⊢ φ \to ((ψ \land χ) \to θ)$
3	2	3impib	$⊢ (φ \land ψ \land χ) \to θ$