Theorem negbii 187

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 152	. . 3 |- (ps -> ph)
3	2	con3i 98	. 2 |- (-. ph -> -. ps)
4	1	biimp 151	. . 3 |- (ph -> ps)
5	4	con3i 98	. 2 |- (-. ps -> -. ph)
6	3, 5	impbi 157	1 |- (-. ph <-> -. ps)

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

This theorem is referenced by:  mtbi 191  mtbir 192  anor 304  ianor 305  ioran 306  pm4.52 307  pm4.54 309  oran 312  anass 439  andi 604  pm5.18 660  pm5.24 672  oplem1 772  19.43 1088  cbvex 1166  sban 1237  sb8e 1262  sbex 1348  necon3abii 1596  ralnex 1653  rexnal 1654  nss 2113  dfpss3 2134  difdif 2166  nssinpss 2240  nsspssun 2241  dfss4 2242  difin 2245  difab 2269  reuun2 2278  ne0f 2287  ssdif0 2327  ssnelpss 2330  difin0ss 2332  inssdif0 2333  rexpr 2429  iundif2 2610  iindif2 2611  notzfaus 2741  nssss 2764  dtru 2772  pwundif 2828  rexxfr 2901  dffr2 2919  efrirr 2928  efrn2lp 2929  epne3 2930  dfwe2 2935  ordtri3or 2979  rexxp 3219  dm0rn0 3330  reldm0 3331  imadif 3574  fn0 3605  tz6.12-2 3739  rdgsucopabn 3947  tz7.48lem 3955  ndmoprcom 4047  1st2val 4095  2nd2val 4096  0nelqs 4298  brsdom 4381  brsdom2 4461  php3 4515  php3OLD 4516  suc11reg 4605  inf3lem6 4618  r1tr 4654  ranklim 4685  rankuni 4698  rankxplim2 4713  rankxplim3 4714  rankxpsuc 4715  kmlem4 4768  zorn 4797  alephon 4865  alephcard 4867  alephnbtwn 4868  alephval3 4903  cfub 4908  cardcf 4911  cflecard 4912  cfle 4913  psslinpr 5135  ltsor 5261  axrrecex 5284  leadd1 5592  dfinfmr 6067  infmsup 6068  arch 6071  infmxrcl 6086  fzneuzt 6518  crne0 6739  dfisum 7191  isumshft 7204  isumshft2 7205  reef11 7408  infxpidmlem8 7559  alephadd 7582  fctopOLD 7650  cctop 7652  clsval2 7685  ntreq0 7708  spwnex3 8655  cosh111lem3 8716  efif1lem5 8734  efif1lem7 8736  avril1 8784  shne0 9371  chnle 9408  nonbool 9596  lnfncon 9990  strlem1 10177  cvbr2t 10210  cvnbtwn2t 10214  cvnbtwn3t 10215  cvnbtwn4t 10216  hatomistic 10289  chrelat2 10292  atabs2 10329  dmdbr5at 10349  intn3an1d 10428  intn3an2d 10429  intn3an3d 10430  cdrci 10494  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584

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