Theorem con2bii 238

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

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

This theorem is referenced by:  iman 256  annim 257  imnan 261  pm4.53 334  pm4.55 336  oran 338  pm5.18OLD 723  nbbn 724  xor3 737  3ianor 870  notfalOLDOLD 1267  alnex 1380  exnal 1385  exanali 1390  19.35 1426  19.41OLD 1449  equs3 1509  equsex 1513  nne 2021  dfral2 2115  dfrex2 2116  rexim 2194  r19.35 2231  ddif 2737  dfun2 2829  dfin2 2830  difin 2831  dfnul2 2877  noel 2879  rab0 2894  disj4 2922  onuninsuci 3921  intirrOLD 4313  rankxplim3 5825  alephgeom 6030  reclem2pr 6309  ltnlei 6754  infdif 8837  infpss 8843  elcls 8980  avril1 10142  bnj30 12395  divalglem8 13703  dftr6 13834  sltval2 13997  axdenselem4 14022  axdenselem7 14025  axfelem11 14041  axfelem12 14042  axfelem15 14045  dfon3 14072  assxor 14279  tnf 14287  boxeq 14314  fimax 15746  elnev 16404  pmodlem2 17308

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 164

Copyright terms: Public domain