Theorem con1bii 237

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	biimpi 168	. . 3 |- (-. ph -> ps)
3	2	con1i 112	. 2 |- (-. ps -> ph)
4	1	biimpri 169	. . 3 |- (ps -> -. ph)
5	4	con2i 113	. 2 |- (ph -> -. ps)
6	3, 5	impbii 174	1 |- (-. ps <-> ph)

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

This theorem is referenced by:  con2bii 238  ianor 329  dfbi3 733  necon1abii 2059  necon1bbii 2060  dfnul3 2878  snprc 3092  opth2 3546  onxpdisjOLD 4069  intirrOLD 4313  dffv2 4734  kmlem3 5929  axpowndlem3 6103  nnunb 7279  largei 11839  dffr5 13831  brsset 14069  brbigcup 14074  FNid 14119  notev 14316  notal 14317  pm10.252 16307  pm10.253 16308  2nexaln 16327  2exanali 16343  elpadd0 17270

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 164

Copyright terms: Public domain