Theorem con1bii 220

Description: A contraposition inference.

Hypothesis

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

Assertion

Ref	Expression
con1bii	|- (-. ps <-> ph)

Proof of Theorem con1bii

Step	Hyp	Ref	Expression
1		con1bii.1	. . . 4 |- (-. ph <-> ps)
2	1	biimp 151	. . 3 |- (-. ph -> ps)
3	2	con1i 96	. 2 |- (-. ps -> ph)
4	1	biimpr 152	. . 3 |- (ps -> -. ph)
5	4	con2i 97	. 2 |- (ph -> -. ps)
6	3, 5	impbi 157	1 |- (-. ps <-> ph)

Syntax hints:  -. wn 2   <-> wb 146

This theorem is referenced by:  con2bii 221  dfbi3 672  necon1abii 1619  necon1bbii 1620  dfnul3 2286  snprc 2447  opth2 2806  onxpdisj 3247  intirr 3447  ecelqsdm 4305  kmlem3 4777  axpowndlem3 4963  nnunb 6072  large 10189

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain