Theorem con2bii 219

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

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

This theorem is referenced by:  iman 235  annim 236  imnan 240  pm4.53 306  pm4.55 308  pm5.18 663  nbbn 664  xor3 677  alnex 1069  exnal 1074  exanali 1079  19.35 1111  19.41 1131  equs3 1186  equsex 1189  nne 1632  dfral2 1701  dfrex2 1702  r19.35 1805  ddif 2221  dfun2 2295  dfin2 2296  dfnul2 2334  noel 2336  disj4 2370  onuninsuci 3194  intirr 3533  rankxplim3 4860  alephgeom 5032  reclem2pr 5311  ltnlei 5733  infdif 7780  infpss 7786  elcls 7914  avril1 9058  fimax 11837

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 145

Copyright terms: Public domain