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 is referenced by:  xor3  346  imnan  411  annim  414  anor  475  pm4.53  478  pm4.55  480  oran  482  3ianor  949  nanan  1289  xnor  1297  xorass  1299  xorneg1  1302  xorneg  1304  alnex  1530  exnal  1561  2exnexn  1567  equs3  1625  19.9v  1663  equsex  1902  nne  2450  dfral2  2555  dfrex2  2556  r19.35  2687  ddif  3308  dfun2  3404  dfin2  3405  difin  3406  dfnul2  3457  rab0  3475  disj4  3503  onuninsuci  4631  omopthi  6655  dfsup2  7195  dfsup2OLD  7196  rankxplim3  7551  alephgeom  7709  ominf4  7938  fin1a2lem7  8032  fin41  8070  reclem2pr  8672  1re  8837  ltnlei  8939  divalglem8  12599  elcls  16810  ist1-2  17075  fin1aufil  17627  dchrelbas3  20477  avril1  20836  nmo  23144  dftr6  24107  sltval2  24310  sltres  24318  nodenselem4  24338  nodenselem7  24341  nofulllem5  24360  dfon3  24432  dffun10  24453  elfuns  24454  axcontlem12  24603  tnf  24952  boxeq  24987  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  wopprc  27123  f1omvdco3  27392  equsexv-x12  29113  cdleme0nex  30479

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

This theorem depends on definitions:  df-bi 177