Theorem con4bid 293

Description: A contraposition deduction. (Contributed by NM, 21-May-1994.)

Hypothesis

Ref	Expression
con4bid.1

Assertion

Ref	Expression
con4bid

Proof of Theorem con4bid

Step	Hyp	Ref	Expression
1		con4bid.1	. . . 4
2	1	biimprd 223	. . 3
3	2	con4d 105	. 2
4	1	biimpd 207	. 2
5	3, 4	impcon4bid 205	1

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

This theorem is referenced by:  notbid  294  notbi  295  had0  1471  necon4abidOLD  2709  sbcne12  3827  sbcne12gOLD  3828  ordsucuniel  6659  rankr1a  8275  ltaddsub  10051  leaddsub  10053  supxrbnd1  11542  supxrbnd2  11543  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  fllt  11943  rabssnn0fi  12095  elcls  19574  rusgranumwlks  24956  chrelat3  27290  wl-sb8et  30001

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