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  2521  dfral2  2627  dfrex2  2628  r19.35  2759  elin  3220  dblcompl  3228  ddif  3399  dfun2  3491  dfin2  3492  difin  3493  dfnul2  3553  rab0  3572  disj4  3600  dfimak2  4299  dfint3  4319  dfpw2  4328  dfaddc2  4382  nndisjeq  4430  ltfinex  4465  ssfin  4471  tfinltfin  4502  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  imasn  5019  brimage  5794  releqmpt2  5810  disjex  5824  funsex  5829  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ltcirr  6273