Theorem con2bii 347

Description: A contraposition inference. (Contributed by NM, 12-Mar-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 214	. . 3 |- ( -. ps <-> ph )
3	2	con1bii 346	. 2 |- ( -. ph <-> ps )
4	3	bicomi 214	1 |- ( ps <-> -. ph )

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

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 197

This theorem is referenced by:  xor3  372  imnan  438  annim  441  anor  510  pm4.53  513  pm4.55  515  oran  517  3ianor  1055  nanan  1449  xnor  1466  xorneg  1476  alnex  1706  exnal  1754  2exnexn  1772  equs3  1875  19.3v  1897  nne  2798  rexnal  2995  dfrex2  2996  r2exlem  3059  r19.35  3084  ddif  3742  dfun2  3859  dfin2  3860  difin  3861  dfnul2  3917  rab0OLD  3956  disj4  4025  snnzb  4254  onuninsuci  7040  omopthi  7737  dfsup2  8350  rankxplim3  8744  alephgeom  8905  fin1a2lem7  9228  fin41  9266  reclem2pr  9870  1re  10039  ltnlei  10158  divalglem8  15123  f1omvdco3  17869  elcls  20877  ist1-2  21151  fin1aufil  21736  dchrelbas3  24963  tgdim01  25402  axcontlem12  25855  avril1  27319  dftr6  31640  sltval2  31809  sltres  31815  nosepeq  31835  nolt02o  31845  nosupbnd2lem1  31861  dfon3  31999  dffun10  32021  brub  32061  bj-exnalimn  32610  bj-modal4e  32705  con2bii2  33180  heiborlem1  33610  heiborlem6  33615  heiborlem8  33617  cdleme0nex  35577  wopprc  37597  1nevenALTV  41602