Theorem impcon4bid 205

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

Hypotheses

Ref	Expression
impcon4bid.1
impcon4bid.2

Assertion

Ref	Expression
impcon4bid

Proof of Theorem impcon4bid

Step	Hyp	Ref	Expression
1		impcon4bid.1	. 2
2		impcon4bid.2	. . 3
3	2	con4d 105	. 2
4	1, 3	impbid 191	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184

This theorem is referenced by:  con4bid  293  soisoi  6224  isomin  6233  alephdom  8483  nn0n0n1ge2b  10885  om2uzlt2i  12062  sadcaddlem  14107  isprm5  14253  pcdvdsb  14392  cvgdvgrat  31194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185