Theorem con2bii 221

Description: A contraposition inference.

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

Syntax hints:  -. wn 2   <-> wb 146

This theorem is referenced by:  iman 237  annim 238  imnan 242  pm4.53 308  pm4.55 310  pm5.18 658  nbbn 659  xor3 672  alnex 1029  exnal 1034  exanali 1039  19.35 1071  19.41 1091  equs3 1145  equsex 1148  nne 1581  dfral2 1647  dfrex2 1648  r19.35 1751  ddif 2159  dfun2 2233  dfin2 2234  dfnul2 2272  noel 2274  disj4 2307  onuninsuc 3098  intirr 3427  rankxplim3 4686  alephgeom 4854  reclem2pr 5129  ltnle 5552  infdif 7511  elcls 7646  avril1 8723

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain