Theorem impcon4bid

Description: A variation on impbid with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009)

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

Proof

Step	Hyp	Ref	Expression
1		impcon4bid.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		impcon4bid.2	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜒 ) )
3	2	con4d	⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
4	1 3	impbid	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )