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

Metamath Proof Explorer

Theorem impbidd

Description: Deduce an equivalence from two implications. Double deduction associated with impbi and impbii . Deduction associated with impbid . (Contributed by Rodolfo Medina, 12-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		impbidd.1	$⊢ φ \to (ψ \to (χ \to θ))$
2		impbidd.2	$⊢ φ \to (ψ \to (θ \to χ))$
3		impbi	$⊢ (χ \to θ) \to ((θ \to χ) \to (χ \leftrightarrow θ))$
4	1 2 3	syl6c	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$