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	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
	impbidd.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜒 ) ) )
Assertion	impbidd	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		impbidd.1	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
2		impbidd.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜒 ) ) )
3		impbi	⊢ ( ( 𝜒 → 𝜃 ) → ( ( 𝜃 → 𝜒 ) → ( 𝜒 ↔ 𝜃 ) ) )
4	1 2 3	syl6c	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )