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 662  nbbn 663  xor3 676  alnex 1035  exnal 1040  exanali 1045  19.35 1077  19.41 1097  equs3 1151  equsex 1154  nne 1592  dfral2 1658  dfrex2 1659  r19.35 1762  ddif 2173  dfun2 2247  dfin2 2248  dfnul2 2286  noel 2288  disj4 2322  onuninsuc 3115  intirr 3448  rankxplim3 4731  alephgeom 4900  reclem2pr 5176  ltnle 5598  infdif 7576  infpss 7582  elcls 7708  avril1 8786

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