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 659  nbbn 660  xor3 673  alnex 1032  exnal 1037  exanali 1042  19.35 1074  19.41 1094  equs3 1148  equsex 1151  nne 1587  dfral2 1653  dfrex2 1654  r19.35 1757  ddif 2166  dfun2 2240  dfin2 2241  dfnul2 2279  noel 2281  disj4 2314  onuninsuc 3104  intirr 3437  rankxplim3 4697  alephgeom 4865  reclem2pr 5140  ltnle 5562  infdif 7528  infpss 7534  elcls 7664  avril1 8739

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