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 602  pm5.18 658  pm5.24 670  oplem1 770  19.43 1084  cbvex 1162  sban 1232  sb8e 1257  sbex 1343  necon3abii 1588  ralnex 1645  rexnal 1646  nss 2103  dfpss3 2124  difdif 2156  nssinpss 2230  nsspssun 2231  dfss4 2232  difin 2235  difab 2259  reuun2 2268  ne0f 2277  ssdif0 2317  ssnelpss 2320  difin0ss 2322  inssdif0 2323  rexpr 2419  iundif2 2600  iindif2 2601  notzfaus 2731  nssss 2754  dtru 2762  pwundif 2817  rexxfr 2891  dffr2 2909  efrirr 2918  efrn2lp 2919  epne3 2920  dfwe2 2925  ordtri3or 2969  rexxp 3209  dm0rn0 3319  reldm0 3320  imadif 3560  fn0 3591  tz6.12-2 3724  rdgsucopabn 3932  tz7.48lem 3940  ndmoprcom 4033  1st2val 4079  2nd2val 4080  0nelqs 4282  brsdom 4363  brsdom2 4441  php3 4495  suc11reg 4577  inf3lem6 4590  r1tr 4626  ranklim 4657  rankuni 4670  rankxplim2 4685  rankxplim3 4686  rankxpsuc 4687  kmlem4 4740  zorn 4769  alephon 4837  alephcard 4839  alephnbtwn 4840  alephval3 4875  cfub 4880  cardcf 4883  cflecard 4884  cfle 4885  psslinpr 5107  ltsor 5233  axrrecex 5256  leadd1 5566  dfinfmr 6014  infmsup 6015  arch 6018  infmxrcl 6033  fzneuzt 6450  nn0opth 6596  crne0 6670  absgt0 6778  dfisum 7127  isumshft 7139  isumshft2 7140  reef11 7349  infxpidmlem8 7502  alephadd 7524  fctop 7592  cctop 7594  clsval2 7627  ntreq0 7650  spwnex3 8579  cosh111lem3 8631  efif1lem5 8649  efif1lem7 8651  avril1 8723  shne0 9286  chnle 9323  nonbool 9513  lnfncon 9905  strlem1 10087  cvbr2t 10120  cvnbtwn2t 10124  cvnbtwn3t 10125  cvnbtwn4t 10126  hatomistic 10197  chrelat2 10200  atabs2 10237  dmdbr5at 10255  intn3an1d 10328  intn3an2d 10329  intn3an3d 10330  cdrci 10381  efilcp 10445  efilcp2 10450  cnfilca 10451

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