Theorem con2bii 322

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem con2bii

Step	Hyp	Ref	Expression
1		con2bii.1	. . . 4 |- (ph <-> -. ps)
2	1	bicomi 193	. . 3 |- (-. ps <-> ph)
3	2	con1bii 321	. 2 |- (-. ph <-> ps)
4	3	bicomi 193	1 |- (ps <-> -. ph)

Syntax hints:  -. wn 3   <-> wb 176

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 177

This theorem is referenced by:  xor3  346  imnan  411  annim  414  anor  475  pm4.53  478  pm4.55  480  oran  482  3ianor  949  nanan  1289  xnor  1306  xorass  1308  xorneg1  1311  xorneg  1313  alnex  1543  exnal  1574  2exnexn  1580  equs3  1644  19.3v  1665  19.9vOLD  1697  equsex  1962  nne  2520  dfral2  2626  dfrex2  2627  r19.35  2758  elin  3219  dblcompl  3227  ddif  3398  dfun2  3490  dfin2  3491  difin  3492  dfnul2  3552  rab0  3571  disj4  3599  dfimak2  4298  dfint3  4318  dfpw2  4327  dfaddc2  4381  nndisjeq  4429  ltfinex  4464  ssfin  4470  tfinltfin  4501  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  imasn  5018  brimage  5793  releqmpt2  5809  disjex  5823  funsex  5828  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  ltcirr  6272