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 603  pm5.18 659  pm5.24 671  oplem1 771  19.43 1087  cbvex 1165  sban 1236  sb8e 1261  sbex 1347  necon3abii 1594  ralnex 1651  rexnal 1652  nss 2110  dfpss3 2131  difdif 2163  nssinpss 2237  nsspssun 2238  dfss4 2239  difin 2242  difab 2266  reuun2 2275  ne0f 2284  ssdif0 2324  ssnelpss 2327  difin0ss 2329  inssdif0 2330  rexpr 2426  iundif2 2606  iindif2 2607  notzfaus 2737  nssss 2760  dtru 2768  pwundif 2824  rexxfr 2897  dffr2 2915  efrirr 2924  efrn2lp 2925  epne3 2926  dfwe2 2931  ordtri3or 2975  rexxp 3215  dm0rn0 3326  reldm0 3327  imadif 3570  fn0 3601  tz6.12-2 3734  rdgsucopabn 3942  tz7.48lem 3950  ndmoprcom 4042  1st2val 4088  2nd2val 4089  0nelqs 4291  brsdom 4372  brsdom2 4450  php3 4504  suc11reg 4588  inf3lem6 4601  r1tr 4637  ranklim 4668  rankuni 4681  rankxplim2 4696  rankxplim3 4697  rankxpsuc 4698  kmlem4 4751  zorn 4780  alephon 4848  alephcard 4850  alephnbtwn 4851  alephval3 4886  cfub 4891  cardcf 4894  cflecard 4895  cfle 4896  psslinpr 5118  ltsor 5244  axrrecex 5267  leadd1 5576  dfinfmr 6024  infmsup 6025  arch 6028  infmxrcl 6043  fzneuzt 6463  nn0opth 6611  crne0 6685  absgt0 6793  dfisum 7144  isumshft 7156  isumshft2 7157  reef11 7366  infxpidmlem8 7519  alephadd 7542  fctop 7610  cctop 7612  clsval2 7645  ntreq0 7668  spwnex3 8612  cosh111lem3 8666  efif1lem5 8684  efif1lem7 8686  avril1 8739  shne0 9326  chnle 9363  nonbool 9553  lnfncon 9946  strlem1 10133  cvbr2t 10166  cvnbtwn2t 10170  cvnbtwn3t 10171  cvnbtwn4t 10172  hatomistic 10245  chrelat2 10248  atabs2 10285  dmdbr5at 10305  intn3an1d 10386  intn3an2d 10387  intn3an3d 10388  cdrci 10440  efilcp 10504  efilcp2 10509  cnfilca 10510

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