Theorem impcon4bid

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

	Ref	Expression
Hypotheses	impcon4bid.1	|- ( ph -> ( ps -> ch ) )
	impcon4bid.2	|- ( ph -> ( -. ps -> -. ch ) )
Assertion	impcon4bid	|- ( ph -> ( ps <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		impcon4bid.1	|- ( ph -> ( ps -> ch ) )
2		impcon4bid.2	|- ( ph -> ( -. ps -> -. ch ) )
3	2	con4d	|- ( ph -> ( ch -> ps ) )
4	1 3	impbid	|- ( ph -> ( ps <-> ch ) )