Theorem impbid1

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007)

	Ref	Expression
Hypotheses	impbid1.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	impbid1.2	⊢ ( 𝜒 → 𝜓 )
Assertion	impbid1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		impbid1.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		impbid1.2	⊢ ( 𝜒 → 𝜓 )
3	2	a1i	⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
4	1 3	impbid	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )