Theorem con4bid 307

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

Hypothesis

Ref	Expression
con4bid.1	|- ( ph -> ( -. ps <-> -. ch ) )

Assertion

Ref	Expression
con4bid	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem con4bid

Step	Hyp	Ref	Expression
1		con4bid.1	. . . 4 |- ( ph -> ( -. ps <-> -. ch ) )
2	1	biimprd 238	. . 3 |- ( ph -> ( -. ch -> -. ps ) )
3	2	con4d 114	. 2 |- ( ph -> ( ps -> ch ) )
4	1	biimpd 219	. 2 |- ( ph -> ( -. ps -> -. ch ) )
5	3, 4	impcon4bid 217	1 |- ( ph -> ( ps <-> ch ) )

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

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 197

This theorem is referenced by:  notbid  308  notbi  309  had0  1543  cbvexdva  2283  sbcne12  3986  ordsucuniel  7024  rankr1a  8699  ltaddsub  10502  leaddsub  10504  supxrbnd1  12151  supxrbnd2  12152  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  fllt  12607  rabssnn0fi  12785  elcls  20877  rusgrnumwwlks  26869  chrelat3  29230  sltrec  31924  wl-sb8et  33334  infxrbnd2  39585  oddprmne2  41624  nnolog2flm1  42384