Theorem con2bii 323

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 194	. . 3 |- ( -. ps <-> ph )
3	2	con1bii 322	. 2 |- ( -. ph <-> ps )
4	3	bicomi 194	1 |- ( ps <-> -. ph )

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

This theorem is referenced by:  xor3  347  imnan  412  annim  415  anor  476  pm4.53  479  pm4.55  481  oran  483  3ianor  951  nanan  1295  xnor  1312  xorass  1314  xorneg1  1317  xorneg  1319  alnex  1549  exnal  1580  2exnexn  1587  equs3  1651  19.3v  1673  19.9vOLD  1706  equsexOLD  1970  nne  2579  dfral2  2686  dfrex2  2687  r19.35  2823  ddif  3447  dfun2  3544  dfin2  3545  difin  3546  dfnul2  3598  rab0  3616  disj4  3644  onuninsuci  4787  omopthi  6867  dfsup2  7413  dfsup2OLD  7414  rankxplim3  7769  alephgeom  7927  fin1a2lem7  8250  fin41  8288  reclem2pr  8889  1re  9054  ltnlei  9158  divalglem8  12883  elcls  17100  ist1-2  17373  fin1aufil  17925  dchrelbas3  20983  avril1  21718  dftr6  25329  sltval2  25532  sltres  25540  nodenselem4  25560  nodenselem7  25563  nofulllem5  25582  dfon3  25654  dffun10  25675  elfuns  25676  axcontlem12  25826  heiborlem1  26418  heiborlem6  26423  heiborlem8  26425  wopprc  26999  f1omvdco3  27268  equsexNEW7  29208  cdleme0nex  30784

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 178