Theorem negbii 162

Description: Negate both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.a	|- (ph <-> ps)

Assertion

Ref	Expression
negbii	|- (-. ph <-> -. ps)

Proof of Theorem negbii

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 |- (ph <-> ps)
2	1	biimpr 134	. . 3 |- (ps -> ph)
3	2	con3i 90	. 2 |- (-. ph -> -. ps)
4	1	biimp 133	. . 3 |- (ph -> ps)
5	4	con3i 90	. 2 |- (-. ps -> -. ph)
6	3, 5	impbi 139	1 |- (-. ph <-> -. ps)

Syntax hints:  -. wn 1   <-> wb 127

This theorem is referenced by:  mtbi 166  mtbir 167  anor 252  ianor 253  ioran 254  oran 255  anass 336  andi 456  pm5.18 497  oplem1 578  19.43 767  cbvex 849  sban 889  sb8e 919  sbex 998  necom 1198  ralnex 1209  rexnal 1210  nss 1550  dfpss3 1558  difdif 1595  nssinpss 1665  nsspssun 1666  dfss4 1667  difin 1670  difab 1693  n0f 1713  rabn0 1716  0pss 1730  ssdif0 1748  ssnelpss 1751  difin0ss 1753  inssdif0 1754  nssss 1866  exss 1881  dtru 1889  iundif2 2032  iindif2 2033  dffr2 2171  efrirr 2180  efrn2lp 2181  epne3 2182  dfwe2 2187  ordtri3or 2230  tfi 2244  orduniorsuc 2337  dm0rn0 2549  reldm0 2550  imadif 2714  fn0 2739  tz6.12-2 2845  rdgsucopabn 2985  tz7.48lem 2993  ndmoprcom 3061  1st2val 3097  0nelqs 3234  brsdom 3286  brsdom2 3363  0sdom 3368  php3 3411  suc11reg 3456  inf3lem6 3469  r1tr 3498  scott0s 3544  cplem1 3545  aceq5lem3 3560  kmlem3 3582  kmlem4 3583  kmlem10 3589  zornlem6 3608  zorn2 3612  alephon 3671  alephcard 3673  alephnbtwn 3674  cfub 3703  cardcf 3706  cflecard 3707  cfle 3708  elni 3798  psslinpr 3929  ltsor 4055  axrecex 4079  axrrecex 4081  leadd1 4314  negne0 4379  nngt1ne1t 4440  arch 4521  elnnz 4572  uzwo3lem1 4614  seqlem2 4663  nn0opth 4724  absgt0 4842  abslem2i 4866  ruclem8 4892  ruclem35 4919  infxpidmlem8 4940  bcs 5101  shne0 5372  chnle 5406  h1de2b 5459  h1de2ctlem 5460  pjnel 5665  strlem1 5691  cvbr2t 5715  cvnbtwn2t 5719  cvnbtwn3t 5720  cvnbtwn4t 5721  hatomistic 5755  chrelat2 5758

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

This theorem depends on definitions:  df-bi 128

metamath.org