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

Metamath Proof Explorer

Theorem bija

Description: Combine antecedents into a single biconditional. This inference, reminiscent of ja , is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im and pm5.21im ). (Contributed by Wolf Lammen, 13-May-2013)

	Ref	Expression
Hypotheses	bija.1	$⊢ φ \to (ψ \to χ)$
	bija.2	$⊢ \neg φ \to (\neg ψ \to χ)$
Assertion	bija	$⊢ (φ \leftrightarrow ψ) \to χ$

Proof

Step	Hyp	Ref	Expression
1		bija.1	$⊢ φ \to (ψ \to χ)$
2		bija.2	$⊢ \neg φ \to (\neg ψ \to χ)$
3		biimpr	$⊢ (φ \leftrightarrow ψ) \to (ψ \to φ)$
4	3 1	syli	$⊢ (φ \leftrightarrow ψ) \to (ψ \to χ)$
5		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
6	5	con3d	$⊢ (φ \leftrightarrow ψ) \to (\neg ψ \to \neg φ)$
7	6 2	syli	$⊢ (φ \leftrightarrow ψ) \to (\neg ψ \to χ)$
8	4 7	pm2.61d	$⊢ (φ \leftrightarrow ψ) \to χ$