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 670  necon1abii 1616  necon1bbii 1617  dfnul3 2283  snprc 2443  opth2 2800  onxpdisj 3241  intirr 3441  ecelqsdm 4299  kmlem3 4767  axpowndlem3 4951  nnunb 6070  large 10194

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